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

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

用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.