基于SMV的滑动窗口协议的形式化建模与分析
Formally Model and Analysis Sliding Window Protocol
本文采用模型检测的方法，在理想信道、信道可能丢失报文、受到入侵攻击这3种情况下，给出了滑动窗口协议的形式化模型，对协议的信息一致性、系统活性、信息完整性等系统属性，进行验证，最后根据实验结果，得出结论：该协议在不同情况下，各系统属性的表现是不同的；协议设计者可以通过SMV提供的反例，找到协议的漏洞，提出应对方案。
his paper proposes a method of model checking, according to three conditions: ideal channel, channel maybe loses message, channel under attack, respectively give out formal model for sliding window protocol, verify the protocol’s property: information-consistence, system liveliness, information-integrity, finally give out the result and draw a conclusion: under different conditions, system property also appear different; protocol designer can find weakness of protocol by analysis counter-example provided by SMV.
赵也非、谢瑾奎、杨宗源
通信
网络协议滑动窗口模型检测SMV协议分析
network protocolsliding windowmodel checkingSMVprotocol analysis
赵也非,谢瑾奎,杨宗源.基于SMV的滑动窗口协议的形式化建模与分析[EB/OL].(2008-03-18)[2025-08-02].http://www.paper.edu.cn/releasepaper/content/200803-472.点此复制
评论