协议分析与设计上机报告

一．实验目的

学习和掌握PROMELA语言，并能在SPIN上对协议进行模

拟和分析。

二．实验题目

6-5 将6.3节描述的协议条件改为报文和应答均会出错，且都丢失，接收方没有无线接收能力，这就是我们通常所说的实

用停等协议。请用PROMELA进行描述，并用SPIN模拟运行、

一般性验证、无进展循环验证和人为加入错误进行验证。

6-6 请根据图6-16写出著名的AB协议的PROMELA描述，

并验证“A”获取的每一个报文至少有一个是正确的，而“B”接收的每一个报文之多有一次是正确的。

Terminal A Terminal B

三．实验分析

6-5 停止等待协议

因为协议条件为报文应答均会出错，且都丢失，接收方没有无限接收能力，所以此时信道应该有5种信号，分别为：信息，ACK，NAK，出错信号和丢失信号，即mtype={Msg,Ack,Nak,Err,Miss}。