基于Spin的Rdt2.2及其改进的形式化分析  

Formalized Analyzing of Protocol Model Called Rdt2.2 base on Spin

作　　者：陈宁军[1] 许博[2] 吴春寒[2] 

机构地区：[1]南京陆军指挥学院作战实验中心,南京210045 [2]解放军理工大学指挥自动化学院计算机系,江苏南京210017

出　　处：《微计算机信息》2009年第15期201-203,共3页Control & Automation

摘　　要：用Promela语言对滑动窗口协议中的Rdt2.2模型进行了描述,通过Spin对该描述进行了形式化分析验证,并发现存在一个死锁。进而对该协议进行改进,采用添加定时器的方法解决了死锁问题,通过这种形式化验证增加了协议的正确性和可靠性。First describe the sliding window protocol model called Rdt2.2 by promela, then formalized analyze the model by tools of Spin and find the protocol model has a deadlock. Later on, settle the problem of deadlock by means of adding timers, in order to improve the model of Rdt2.2. Finally, the veracity and reliability of protocol model are improved effectively by means of formalized analyzing.

关 键 词：SPIN PROMELA 形式化分析 Rdt2.2 死锁 

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]