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

摘要：

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

关键词：Spin、Promela、形式化分析、Rdt2.2、死锁

所属期刊栏目：25

分类号：TP311.5(计算技术、计算机技术)

在线出版日期：2009-06-19（万方平台首次上网日期，不代表论文的发表时间）

页数：共3页

页码：201-203