| 基于Spin的Rdt2.2及其改进的形式化分析 |
| |
| 引用本文： | 陈宁军,许博,吴春寒.基于Spin的Rdt2.2及其改进的形式化分析[J].微计算机信息,2009,25(15). |
| |
| 作者姓名： | 陈宁军 许博 吴春寒 |
| |
| 作者单位： | 陈宁军,CHEN Ning-jun(京南京陆军指挥学院作战实验中心,210045);许博,吴春寒,XU Bo,WU Chun-han(苏南京解放军理工大学指挥自动化学院计算机系,210017)
|
| |
| 摘 要： | 用Promda语言对滑动窗口协议中的Rdt2.2模型进行了描述,通过Spin对该描述进行了形式化分析验证,并发现存在一个死锁.进而对该协议进行改进,采用添加定时器的方法解决了死锁问题,通过这种形式化验证增加了协议的正确性和可靠性.
|
| 关 键 词： | 形式化分析 死锁 |
Formalized Analyzing of Protocol Model Called Rdt2.2 base on Spin |
| |
| CHEN Ning-jun,XU Bo,WU Chun-han.Formalized Analyzing of Protocol Model Called Rdt2.2 base on Spin[J].Control & Automation,2009,25(15). |
| |
| Authors: | CHEN Ning-jun XU Bo WU Chun-han |
| |
| Abstract: | |
| |
| Keywords: | Spin Promela Rdt2 2 |
| 本文献已被 万方数据 等数据库收录！ |
|
