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

• 作者: 吴春寒 许博 陈宁军
• 来源期刊: 科技与创新
• 关键词: Spin Promela 形式化分析 Rdt2.2 死锁
• 年，卷（期）: 2009,（15）
• 所属期刊栏目: 软件时空
• 页码范围: 201-203
• 页数: 3页
• 分类号: TP311.5
• 语种: 中文
• DOI: 10.3969/j.issn.1008-0570.2009.15.082

摘要

用Promda语言对滑动窗口协议中的Rdt2.2模型进行了描述,通过Spin对该描述进行了形式化分析验证,并发现存在一个死锁.进而对该协议进行改进,采用添加定时器的方法解决了死锁问题,通过这种形式化验证增加了协议的正确性和可靠性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	陈宁军	京南京陆军指挥学院作战实验中心	1	0	0.0	0.0
2	许博	苏南京解放军理工大学指挥自动化学院计算机系	1	0	0.0	0.0
3	吴春寒	苏南京解放军理工大学指挥自动化学院计算机系	1	0	0.0	0.0