《网络协议分析与设计》实验报告书 实验二

一、实验目的 1.熟悉AB协议，并能用PROMELA语言正确描述 2.掌握用SPIN验证协议的方法 二、实验原理 对于给定的一个使用PROMELA描述的协议系统，SPIN可以对其执行任意的模拟，也可以生成一个C代码程序，然后对该系统的正确性进行有效检验，并报告系统中出现的死锁，无效的循环，未定义的接受和标记不完全等情况。 三、实验仪器 PC机 四、实验内容 请根据下图写出著名的 AB 协议的 PR

>>阅读原文<<