参考教材:《网络协议工程》吴礼发,电子工业出版社,2011.4
实验环境:Ubuntu 18.04.1 LTS,Windows 10,VMware 15.0.2。
(一)Spin入门(iSpin究竟是怎么装上去的?是tar.gz的install.sh还是sudo apt install spin?)
Ubuntu下直接一句sudo apt install spin,就不make了。基本就装好Spin了,想要最新版Spin的话就手动下载:
Spin - Formal Verification
http://spinroot.com/spin/whatispin.html
点击下方download,进入界面后下载spin649_linux64.gz。
拷贝到虚拟机桌面,gunzip解压后鼠标右键点击解压后的文件,将它重命名为spin,复制到/usr/bin下:
查看版本,回显6.4.9说明一切顺利:
其他需要安装的:(有些可能装过了,不管咋样挨个试一遍都装没装全)
sudo apt-get install byacc
sudo apt-get install tcl
sudo apt-get install tk8.5
sudo apt-get install graphviz //可以图形化显示运行结果
sudo apt-get install pan
(二)小试牛刀
打开iSpin,先实验个简单的数据链路层RDT 1.0协议(书P152)
(这在里面输代码对齐不咋方便,不如在VS2017里输好了直接拷进来,再打开)
点击菜单栏的Simulate/Replay,设定maximum number of steps=300,点击“(Re)Run”开始模拟:
下面中间的黑色窗口是命令行形式,如果在shell里执行iSpin右上角显示的Background command executed,得到的结果就是中间窗口里的样子。
再看时序图,SENDER和RECEIVER都是0→1→2→0→……不断循环,这正是RDT 1.0协议:信道没有误码,也不会丢失报文,接收方有无限接受能力,一方发送,一方接收。这是个理想状态下的协议。
接下来看看一般性验证:点击菜单栏Verification,选择“safety”,点击Run,结果如下图,结果基本与书中P154图6-3一致。
无进展循环验证则点击Liveness中的non-progress cycles,再点击一次Run,结果如下图所示,与书中P154图6-4一致:
(三)实验一:思考题6-5
报文和应答均会出错,且都丢失,接收方没有无限接收能力——实用的停等协议。请用PROMELA进行描述,并用SPIN模拟运行、一般性验证、无进展循环验证和人为加入错误进行认证。
参考链接:
1.模型检测工具spin在ubuntu下的安装方法 - 泥瓦匠的专栏 - CSDN博客
https://blog.csdn.net/tiefanhe/article/details/8176418