参考教材：《网络协议工程》吴礼发，电子工业出版社，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
报文和应答均会出错，且都丢失，接收方没有无限接收能力——实用的停等协议（Stop-and-Wait Protocol）。请用PROMELA进行描述，并用SPIN模拟运行、一般性验证、无进展循环验证和人为加入错误进行认证。
引用参考链接2：在这里设为 Miss，且在接受方和发送方的两个进程中添加可能收到Miss信息的情况：当发送方收到Miss时，与收到Err的情况相同，都重发上一个数据；当接受方接收到Miss时，则直接跳过。
if下::是可能执行的选项，一般都设置了3个：正常接收/发送，出错，丢失。
代码我努力对齐了，并列的代码是一个级别的，希望大家能看懂。
#define MAXSEQ 5
mtype = { Msg,ACK,NAK,Err,Miss };
chan SenderToReceiver = [1] of { mtype,byte,byte };
chan ReceiverToSender = [1] of { mtype,byte,byte };
proctype SENDER(chan InCh, OutCh)
{
byte SendData; //发送的数据
byte SendSeq; //发送的序号
byte ReceivedSeq; //接收到的报文序号
SendData = MAXSEQ - 1;
do
::SendData = (SendData + 1) % MAXSEQ;
again:
if
::OutCh!Msg(SendData, SendSeq) //正常发送数据
::OutCh!Err(0, 0) //模拟发送的报文出错
::OutCh!Miss(0, 0) //模拟发送的报文丢失
fi;
if
::timeout -> goto again //ACK超时，重发报文
::InCh ? Miss(0, 0)-> goto again //ACK丢失，重发报文
::InCh ? Err(0, 0)-> goto again //收到ACK误码，重发报文
::InCh ? NAK(ReceivedSeq, 0)-> //收到NAK，重发报文
end1 : goto again
::InCh ? ACK(ReceivedSeq, 0)->
if
::(ReceivedSeq == SendSeq)-> goto progress //收到ACK且序号正确-->发送下一报文
::(ReceivedSeq != SendSeq)-> //收到ACK但序号不对-->重发前一个报文
end2 : goto again
fi;
fi;
progress: SendSeq = 1 - SendSeq; //产生下一个报文的发送序号
od;
}
proctype RECEIVER(chan InCh, OutCh)
{
byte ReceivedData; //接收到的报文数据
byte ReceivedSeq; //接收到的报文序号
byte ExpectedData; //期望接收到的报文数据
byte ExpectedSeq; //期望接收到的报文序号
do
::InCh ? Msg(ReceivedData, ReceivedSeq)-> //接收报文
if
::(ReceivedSeq == ExpectedSeq)->assert(ReceivedData == ExpectedData); //报文按序到达，准备发送ACK
progress: ExpectedSeq = 1 - ExpectedSeq;
ExpectedData = (ExpectedData + 1) % MAXSEQ;
if
::OutCh!Miss(0, 0) //模拟RECEIVER发送ACK后丢失
ExpectedSeq = 1 - ExpectedSeq;
ExpectedData = (ExpectedData + 4) % MAXSEQ;
::OutCh!ACK(ReceivedSeq, 0)
::OutCh!Err(0, 0) //模拟ARECEIVER发送的ACK出错
ExpectedSeq = 1 - ExpectedSeq;
ExpectedData = (ExpectedData + 4) % MAXSEQ;
fi;
::(ReceivedSeq != ExpectedSeq) //报文失序到达
if
::OutCh!NAK(ReceivedSeq, 0) //发送NAK
::OutCh!Err(0, 0) //模拟ARECEIVER发送的NAK出错
::OutCh!Miss(0, 0) //模拟RECEIVER发送NAK后丢失
fi;
fi;
::InCh ? Err(0, 0)-> //SENDER发来的报文出错了
if
::OutCh!NAK(ReceivedSeq, 0)
::OutCh!Err(0, 0)
::OutCh!Miss(0, 0)
fi;
::InCh ? Miss(0, 0)->skip; //SENDER()发来的报文丢失了
od;
}
init
{
atomic
{
run SENDER(ReceiverToSender, SenderToReceiver);
run RECEIVER(SenderToReceiver, ReceiverToSender);
}
}
Automata意思是自动机，打开代码后点击右上方Automata View出现所有进程，点击其中一个出现如图所示的自动机图示。
(1)模拟运行：
接着就是Simulate/Replay， (Re)Run。
从时序图可以看到第一次进行了一轮正常的收发消息，第二轮SENDER()丢失了报文，第三轮RECEIVER()给SENDER的ACK丢了。
（2）一般性验证
点击Verification，选择Safety，点击Run。
（3）无进展循环验证
选择Liveness下的non-progress cycles，点击Run。
（4）人为加入错误验证
SENDER()部分：goto again改成goto progress，丢包了也当没事直接就操作序号了。
再一次模拟运行：
设定的是能跑10000步的，到139就出错了，仔细一看Msg序号出现3了，显然是不对了。
（四）实验二
题目：根据下图写出著名的AB协议的PROMELA描述，并验证“A获取的每一个报文至少有一次是正确的，而B接收的每一个报文至多有一次是正确的（Every message fetched by A is received error-free at least once and accepted at most once by B）”。
（五）实验三
题目：用PROMELA描述Go-Back-N协议并进行验证。
Go-Back-N协议在数据链路层定义过，但现在消失了，现在实际上是作为一个传输层的协议（Data Communications and Networking FIFTH EDITION 23.2.3, Forouzan）。
参考链接：
1.模型检测工具spin在ubuntu下的安装方法 - 泥瓦匠的专栏 - CSDN博客
https://blog.csdn.net/tiefanhe/article/details/8176418
2.网络协议分析上机报告 - 简书
https://www.jianshu.com/p/3a75b3b0cf83
