网络协议工程SPIN实验报告.doc

网络协议工程SPIN实验报告
摘　要:本文主要介绍了一种基于模型检测的协议自动分析工具SPIN的使用。对经典的AB协议在理想状态、信道有误码无丢失和信道有误码有丢失三种不同环境中分别进行建模，并运用SPIN进行自动分析。在信道有误码有丢失的情况中，我们分别设置了两种错误,以进一步观察协议的运行，分析协议存在的问题。从而加深对协议验证技术和形式化描述技术的认识和理解，进一步掌握运用PROMELA语言对协议进行建模，同时掌握SPIN的基本操作，熟悉运用SPIN对网络协议进行分析，提高实验能力.
关键词：模型检测；AB协议;SPIN。
0.引言
随着计算机通信与网络技术的迅猛发展，网络技术在人们日常的工作、学习和生活的各个方面都得到了普遍地运用。各种网络通信系统在提供越来越丰富的功能的同时，其设计和实现也日益复杂。面对复杂网络系统的挑战，传统的自然语言进行的协议描述，虽然具有表达能力强、可读性好、方便的优点，但是存在不严格、不精确、没有描述标准和存有二义性等缺点.形式化方法使得对网络通信系统的描述、实现和测试变得容易，在对于协议实现、测试的自动化和协议验证上得到了广泛运用.
本文主要介绍一种基于模型检测的协议自动分析工具SPIN及其在分析网络协议中的应用。
1.SPIN概述
随着计算机通信与网络技术的迅猛发展，网络技术在人们日常的工作、学习和生活的各个方面都得到了普遍运用。各种网络通信系统在提供越来越丰富的功能的同时，其设计和实现也日益复杂。面对复杂网络系统的挑战，传统的自然语言进行的协议描述,虽然具有表达能力强、可读性好、方便等优点，但是存在不严格、不精确、没有描述标准和存有二义性等缺点.形式化方法使得对网络通信系统的描述、实现和测试变得容易，在对于协议实现、测试的自动化和协议验证上得到了广泛运用.
本文主要介绍一种基于模型检测的协议自动分析工具SPIN及其应用。
1.1 SPIN概述
SPIN(Simple PROMELA Interpreter）是一种用丁对并发系统验证模型检测器，采用深度优先搜索算法，偏序化简和on—the-fly策略从不同的角度来解决模型检测方法中普遍存在的状态空间爆炸问题,其适合对协议验证.SPIN支持随机、交互和指导性的自动机验证，它主要针对设计规范进行检测。最早是由贝尔实验室的形式化方法与验证小组于1980年开始开发的。1995年偏序简约和线性时态逻辑转换的引入使得SPIN的功能进一步扩大。2001年推出的SPIN4。0版本支持C代码的植入,应用的灵活性进一步增强。随后2003年推出的SPIN4.1版本加入了深度优先搜索算法，2009年连续推出SPIN5.2版本，这使得SPIN的发展又上一个新台阶。NASA使用SPIN检测在1996年火星探测者所存在的错误,结果发现一些错误是可以在发射之前就可以被检测并改正的。SPIN从此就被用来检测土星火箭控制软件和一些应用与外层空间的程序。因SPIN有良好的算法设计和非凡的检测能力，得到了ACM（Association for Computing Machinery）(世界最早的专业计算机协会)的认可，在2001年授予SPIN的开发者Holzmann享有声望的软件系统奖。迄今为止SPIN也是唯一获得ACM软件系统奖的模型检测工具.
SPIN通过模仿系统的执行并产生C程序，探测系统的状态空间，最终验证系统的属性是否满足，如不满足，通过提供系统轨迹的形式帮助使用者找出违反正确性属性的状态.SPIN作为一种形式化自动验证工具，其目的是：提供系统建模语言，用于直观、明确地描述系统模型规约,而不考虑具体实现细节；功能强大而简明的描述系统应满足性质属性要求的逻辑表示法：提供一套验证系统建模逻辑一致性及系统是否满足所要验证性质的方法。它以PROMELA为输入语言，用线性时态逻辑（LTL)公式描述系统必须满足的性质。SPIN可以对大型的协议系统进行有效的正确性分析,即使这个系统覆盖了最大限度的状态空间。SPIN首先从一个描述的协议系统的高层模型规格开始,经分析没有语法错误后，对系统的交互进行模拟，直到确认系统设计拥有预期的行为;然后,SPIN将产生一个明C语言描述的验证程序，经检验器编译后被执行，执行中如果发现了违背正确性说明的任何反例，则可反馈给交互模拟机，通过重现细节剔除引起错误的原因。图1—1描述了SPIN模拟和检测的过程。
PROMELA解析器
LTL公式解析和转换器
SPIN
语法错误报告
验证机产生器
交互模拟
模型优化测试器
执行on-the-fly验证
反例
图1-1 SPIN模拟和检测的过程

1。2 SPIN安装及使用
SPIN可以在很多平台上运行,具有很多版本,我们在这个实验中是在Windows7 64位操作系统中，基于Cygwin linux模拟器中实现的，下面是简要的安装过程。
1。软件准备：
（1）在http://spinroot。com/spin/Src/index。html网页上下载Full distribution， with sources版本，最新版本是6。44，下载的文件名为:spin644.tar.gz。
解压后，里面文件内容：
（2）下载并运行cygwin软件，选择64位windows版本。选择默认参数安装。
需要注意以下几点：
a.选择下载站点要选择等国内镜像站点，加快下载速度。
b.需要选择相应的安装组件：（binutils 、bison、 byacc、xinit、x—org-server、m4、tcl等)
选择红色框部分，展开

分别选择：binutils 、bison、 byacc
继续选择：
继续选择：make
退到上一层,选择展开x11选项：

继续选择：下面2项
然后，退回上层，搜素m4
在结果中选择安装
搜素tcl，选择相应包（tcl是运行图形界面ISPIN的必须环境）。
点击下一步，等待安安装完成.
最后选择创建桌面和开始菜单文件，完成安装。
3）安装完cygwin后，在系统盘(C盘)会有文件夹，进入：c:/cygwin64/bin中,将第一步已解压的SPIN文件夹复制进来，并改名为Spin1。
进入Spin1文件夹中的iSpin文件夹，复制ispin。tcl至外面的bin目录中，并去掉.tcl后缀。
c。编译配置ISPIN
安装完cygwin后，先在windows7命令行运行：C:\〉set CYGWIN=tty notitle glob，
打开cygwin的控制台程序：
进入到spin源码目录中c：/cygwin64/bin/spin1/src
然后进行make：(如果编译不成功,往往因为cygwin编译环境没装好，重新检查安装环节组件的选择）
输入命令：make –f makefile
成功后,src目录里会产生spin.exe，将其复制到bin目录中。
测试tcl环境(如果找不到相应文件，则无法运行ISPIN，重新检查安装环节tcl组件的选择)
输入命令：Which tclsh
输入命令:Which wish
d.运行ISPIN
运行开始-〉cygwin-x->xwin server
桌面右下角会出现当前的x server的虚拟桌面编号(:2。0)
在cygwin的控制台中指定ISPIN运行界面的虚拟桌面编号
输入命令：export DISPLAY=：2.0
运行ISPIN
输入命令：ispin
这样就可以使用ISPIN.
2.实例分析
本次实验主要分析AB协议，分别针对理想状态、信道有误码无丢失和信道有误码有丢失,三种不同的通信环境,设计测试三组实验。在第三组实验过程中，又进行了协议的两种错误处理.
2。1AB协议简介
AB(Alternating Bit）协议是最早的端到端通信协议之一.在AB协议系统中，包含有发送端和接收端两个实体。发送端协议实体从发送方获取一个报文，将序号寄存器值赋给报文，然后向接收端实体发出报文,发送方发出报文之后启动超时计时器，等待确认报文。如果在给定的时间内没有收到确认报文，则重发该报文。如果收到确认报文,其序号与发出报文序号相同，则序号寄存器的内容加l模2，然后发送端实体从发送方用户获取下一个报文；如果收到否定的确认报文，则重发该报文；接收端协议实体在收到报文后，如果确认报文无错误，并且序号和序号寄存器的值相等，则向发送端实体发送确认报文(认可报文的序号值等于接收报文的序号值）,然后将报文递交给接收方用户，序号寄存器的内容加l模2。如果接收的报文有错误，或者序号不正确,则发送否定确认报文。
2.2理想状态下的AB协议实验
在理想状态下，信道没有误码，没有丢失，接收方有无限接收能力。这种状态下，协议比较简单，一方发送，一方接收，不设超时计时器,不进行报文确认.下面是协议的PROMELA描述模型.
1 #define MAXSEQ 3
2 chan SenderToReceiver=[1] of{int}； //只含有1个int类型的通道
3
4 proctype SENDER(） //发送方
5 ｛
6 int seq=0；
7 end: do
8 :：SenderToReceiver!seq； //发送序号
9 process： seq=（seq+1）％MAXSEQ； //
10 od;
11
12 }
13
14 proctype RECEIVER() //接收方
15 ｛
16 int Data；
17 end1： do
18 :：SenderToReceiver？Data； //从通道接收数据
19 od；
20 ｝
21 //—-—-——————-————-————开始运行协议—————--—-———--—-—-——--—
22 init
23 {
24 atomic //原子操作
25 ｛
26 run SENDER（）;
27 run RECEIVER();
28 }
29 ｝
将上述代码保存为RTD1.pml，在ISPIN中打开,点击Syntax Check进行语法错误检测，如图所示，没有语法错误。
然后选择verification选项卡，进行模型验证，模型验证分成三块,safety、liveness、以及LTL never claims。刚开始我们先对程序进行安全性和可活动性验证，下面截图中用的是默认勾选的选项，第一个表示死锁，进程无法执行下去,第二个表示程序的断言冲突（在RTD1.pml中不包含断言)，第三个是允许循环，就是允许只有一个进程一直处于活动状态,而另一个不动。
点击run进行验证，如图所示，没有存在error。Unreached说明两个进程一直在循环运行。
点击Simulate/Replay，进行模拟重放，点击(Re）Run,可以形象地观察协议运行过程。发送方按0，1，2有序发送，接收方按0，1,2有序接收。
2.3 信道有误码、无丢失下的AB协议实验
在此实验中,我们考虑收发信道都产生误码，但没有发生丢包的情形。分别用进程SENDER和RECEIVER来对AB协议的发送端和接收端进行建模：通过进程SENDER的发送语句“OutCh！Msg(SendData,SendSeq)”和“OutCh！Err(8,8)"分别模拟正确传送和误码两种情况；通过进程RECEIVER的发送语句“OutCh!Ack（ReceivedSeq,0)"、OutCh!Nak(ReceivedSeq,0）和“OutCh!Err(8,8）”来分别模拟确认报文、否定确认报文和回执报文发送误码三种情况。在SENDER和RECEIVER进程中使用了assert语句来检验在可能会发生任意的消息丢失的情况下，数据是否能全部按顺序正确地传送到接收端。在SENDER和RECEIVER进程中使刚progress状态标记两端传送确实的数据所必须要执行的语句。因为有可能发送端和接收端只在某些无效的状态中循环，使用progress标记可以在检测过程中检测出没有任何实质意义的不可推进的循环。
下面是协议的PROMELA描述模型.
1 #define MAXSEQ 5
2
3 mtype=｛Msg,Ack，Nak,Err｝;
4
5 chan SenderToReceiver=[1] of {mtype，byte,byte}；
6 chan ReceiverToSender=[1］ of {mtype,byte,byte}；
7
8 proctype SENDER（chan InCh，OutCh)
9 ｛
10 byte SendData；//发送的数据
11 byte SendSeq;//发送序号
12 byte ReceivedSeq；//接收序号
13 SendData=MAXSEQ—1;//下一个要发送的序号
14 do
15 ：：SendData=(SendData+1)％MAXSEQ； //下一个消息
16 again:if
17 ：：OutCh！Msg（SendData,SendSeq） //正确发送数据
18 :：OutCh!Err（8,8） //出现误码
19 fi；
20
21 if
22 :：InCh？Nak(ReceivedSeq,0)-〉
23 end： goto again //收到否定确认，重传
24 ：：InCh?Err(8,8）-> goto again //收到ACK误码，重传
25 ：：InCh?Ack(ReceivedSeq,0）—〉 //收到肯定确认
26 if
27
28 :：(ReceivedSeq==SendSeq）—〉goto progress //确认号正确,传下一报文
29 ：:（ReceivedSeq!=SendSeq)-〉
30 end1: goto again //确认号有误，重传
31 fi
32 fi;
33 progress: SendSeq=1-SendSeq； //产生下一个报文序号
34 od;
35 ｝
36
37 proctype RECEIVER(chan InCh，OutCh)
38 {
39 byte ReceivedData; //接收的数据
40 byte ReceivedSeq; //接收的序号
41 byte ExpectedData； //期望的数据
42 byte ExpectedSeq； //期望的序号
43
44 do
45 ：：InCh?Msg（ReceivedData，ReceivedSeq）->
46 if
47 :：(ReceivedSeq==ExpectedSeq)-> //数据按序到达，发送确认报文
48 assert（ReceivedData==ExpectedData); //检验数据是否能按顺序传送到接收端
49 progress： ExpectedSeq=1—ExpectedSeq；
50 ExpectedData=（ExpectedData+1)％MAXSEQ；
51 if
52 ：：OutCh!Ack(ReceivedSeq，0); //ACK报文正确
53 ：:OutCh！Err(8,8）; //模拟ACK报文误码
54 ExpectedSeq=1-ExpectedSeq；
55 ExpectedData=(ExpectedData+4)％MAXSEQ;
56 fi
57
58 ：：(ReceivedSeq!=ExpectedSeq) —>
59 if
60 ：：OutCh！Nak(ReceivedSeq,0）； //数据不按序到达，发送否定确认报文
61 ：:OutCh!Err(8,8）; //模拟ACK报文误码
62 fi
63 fi
64 ：：InCh?Err —> OutCh！Nak（ReceivedSeq,0)； //数据错误，发送否定确认报文
65 od；
66 }
67
68
69 init
70 ｛
71 atomic //原子操作，执行过程不允许打断
72 {
73 run SENDER（ReceiverToSender,SenderToReceiver);//发送者
74 run RECEIVER(SenderToReceiver,ReceiverToSender）； //接收者
75 }
76 }
将上述代码保存为RTD2.pml，在ISPIN中打开，点击Syntax Check进行语法错误检测，没有语法错误.然后选择verification选项卡，进行模型验证，点击run进行验证，如图所示，没有存在error。Unreached说明两个进程一直在循环运行。
点击Simulate/Replay，进行模拟重放,点击（Re）Run,可以形象地观察协议运行过程.从图中,我们可以直观的看到否定确认、正确确认、回执产生误码和发送报文产生误码的情况。
否定确认
确认报文
回执误码
发送误码

2。4信道有误码、有丢失下的AB协议实验
在此实验中，我们考虑收发信道都产生误码,并且都有发生丢包的情形。分别用进程SENDER和RECEIVER来对AB协议的发送端和接收端进行建模:通过进程SENDER的发送语句“OutCh!Msg（SendData,SendSeq)"、“OutCh！Err（8，8)”和“skip”分别模拟正确传送、误码和丢包三种情况；通过进程RECEIVER的发送语句“OutCh！Ack(ReceivedSeq,0）"、“OutCh!Nak（ReceivedSeq,0）”、“OutCh！Err（8,8）”和“skip”来分别模拟确认报文、否定确认报文、回执报文发送误码和回执报文丢失三种情况。进程RECEIVER中，对正确接收的报文回执时，产生回执报文误码“OutCh!Err(8,8) "和丢包“skip”的情况，应该用“ExpectedSeq=1—ExpectedSeq；ExpectedData=（ExpectedData+4）％MAXSEQ；”，来还原因前一个数据包正确接收而更改的“ExpectedSeq”和“ExpectedData”的值，否则会因为期望接收序号与实际接收序号不一致而一直处于回执“OutCh！Nak(ReceivedSeq,0)”的情况。在SENDER和RECEIVER进程中使用了assert语句来检验在可能会发生任意的消息丢失的情况下，数据是否能全部按顺序正确地传送到接收端。在SENDER和RECEIVER进程中使刚progress状态标记两端传送确实的数据所必须要执行的语句.因为有可能发送端和接收端只在某些无效的状态中循环，使用progress标记可以在检测过程中检测出没有任何实质意义的不可推进的循环。
在此实验中，我们分别模拟了两种错误情况：一是发送方对否定确认报文的忽略，二是接收方在回执发生丢包时,未及时还原期望接收数据和期望接收序号。
下面是协议的PROMELA描述模型。
1 ＃define MAXSEQ 5
2
3 mtype=｛Msg,Ack,Nak，Err}；
4
5 chan SenderToReceiver=［1］ of ｛mtype,byte,byte｝；
6 chan ReceiverToSender=[1］ of {mtype，byte,byte}；
7
8 proctype SENDER(chan InCh，OutCh)
9 ｛
10 byte SendData；//发送的数据
11 byte SendSeq;//发送序号
12 byte ReceivedSeq;//接收序号
13 SendData=MAXSEQ-1;//下一个要发送的序号
14 do
15 ::SendData=（SendData+1)%MAXSEQ; //下一个消息
16 again:if
17 ：:OutCh！Msg(SendData，SendSeq) //正确发送数据
18 ：:OutCh!Err(8,8) //出现误码
19 :：skip //报文丢失
20 fi;
21
22 if
23 ：:timeout -> goto again //超时重传
24 :：InCh?Nak(ReceivedSeq,0）—>
25 end： goto again //收到否定确认，重传
26 ：：InCh?Err（8，8）—> goto again //收到ACK误码，重传
27 ：：InCh？Ack(ReceivedSeq,0）-〉 //收到肯定确认
28 if
29
30 ::（ReceivedSeq==SendSeq)->goto progress //确认号正确，传下一报文
31 :：（ReceivedSeq!=SendSeq）-〉
32 end1： goto again //确认号有误，重传
33 fi
34 fi;
35 progress： SendSeq=1-SendSeq; //产生下一个报文序号
36 od;
37 }
38
39 proctype RECEIVER（chan InCh,OutCh）
40 ｛
41 byte ReceivedData； //接收的数据
42 byte ReceivedSeq； //接收的序号
43 byte ExpectedData； //期望的数据
44 byte ExpectedSeq； //期望的序号
45
46 do
47 :：InCh？Msg(ReceivedData，ReceivedSeq）-〉
48 if
49 ：:（ReceivedSeq==ExpectedSeq）—〉 //数据按序到达，发送确认报文
50 assert（ReceivedData==ExpectedData); //检验数据是否能按顺序传送到接收端
51 progress： ExpectedSeq=1-ExpectedSeq;
52 ExpectedData=（ExpectedData+1）％MAXSEQ;
53 if
54 ：：OutCh！Ack（ReceivedSeq,0)； //ACK报文正确
55 :：OutCh!Err(8，8); //模拟ACK报文误码,并还原期望的序号和数据
56 ExpectedSeq=1—ExpectedSeq;
57 ExpectedData=(ExpectedData+4)％MAXSEQ；
58 ::skip //报文丢失,并还原期望的序号和数据
59 ExpectedSeq=1-ExpectedSeq;
60 ExpectedData=（ExpectedData+4)％MAXSEQ；
61 fi
62
63 ：:(ReceivedSeq！=ExpectedSeq) -〉
64 if
65 ：：OutCh！Nak(ReceivedSeq，0）； //数据不按序到达，发送否定确认报文
66 ::OutCh!Err(8，8）; //模拟ACK报文误码
67 ::skip //报文丢失
68 fi
69 fi
70 ：：InCh？Err(8,8） -〉 OutCh！Nak（ReceivedSeq，0); //数据错误,发送否定确认报文
71 od；
72 ｝
73
74
75 init
76 {
77 atomic //原子操作，执行过程不允许打断
78 {
79 run SENDER(ReceiverToSender,SenderToReceiver）；//发送者
80 run RECEIVER(SenderToReceiver，ReceiverToSender）； //接收者
81 }
82 ｝
将上述代码保存为RTD3。pml，在ISPIN中打开，点击Syntax Check进行语法错误检测,没有语法错误。
然后选择verification选项卡,进行模型验证，点击run进行验证，如图所示，没有存在error.Unreached说明两个进程一直在循环运行。
点击Simulate/Replay,进行模拟重放，点击（Re)Run,可以形象地观察协议运行过程。从图中，我们可以直观的看到丢包、否定确认、正确确认、回执产生误码和发送报文产生误码的情况.
丢包
回执误码
发送误码
正确确认
否定确认

2.4。1下面来观察两种错误的处理。
1。发送方对否定确认报文的忽视
如果我们修改25行中,对否定确认报文正确的处理应该是重传,而改为忽视，不重传,还是继续发送下一个数据，则在进行模型验证时，会产生一个错误“assertion violated (ReceivedData==ExpectedData） （at depth 121)”，我们在程序中第50行用assert标记进行检验数据是否能按顺序传送到接收端时，系统产生违反这一检测的错误。
在进行Simulate/Replay，进行模拟重放，在Mode选项页中，会自动勾选Guided，with trail，ISPIN会将错误的运行结果存储到RTD3。pml.trail文件中，点击（Re）Run进行回放，在运行到最后一步时，我们从变量窗口发现:
RECEIVER（2）:ExpectedData = 0
RECEIVER（2）:ExpectedSeq = 0
RECEIVER（2)：ReceivedData = 2
RECEIVER(2):ReceivedSeq = 0
SENDER(1）：ReceivedSeq = 1
SENDER(1)：SendData = 2
SENDER(1）:SendSeq = 0
对于接收者RECEIVER（)来说，期望接收到的数据是0，但是实际接收到的数据为2，两者不一致，所有系统提示，违反了约束条件。
spin： RDT3.pml:50, Error： assertion violated
spin: text of failed assertion： assert(（ReceivedData==ExpectedData))
而这一错误正式我们对否定确认的忽视造成的。
2.接收方发送确认报文丢失后，未还原相关参数
如果我们忽略59、60行中还原接收方期望接收的数据和序号，即将这两行程序注释，不执行ExpectedSeq=1—ExpectedSeq; ExpectedData=（ExpectedData+4)%MAXSEQ；在进行模型验证时，未发现错误。但是在具体运行的时候会有问题。
点击Simulate/Replay，进行模拟重放，在Mode选项页中,我们勾选Random,with seed,点击（Re)Run观察协议运行状态，我们会发现，发送方和接收方会一直停留在处理Msg（1，1）上而不能往下推进。
运行2600多步
一直停留在Msg(1,1)

下面,我们定位到Eeceiver第一次产生确认报文丢包的第70步，
我们发现，第70步时，接收方正取接收了Msg(1,1)，即接收到了数据1，序号1。此时接收方期望的数据和序号与实际接收的一致。接收方根据协议更新期望的数据和序号。
接着在回执过程中产生丢包，发送方在计时器超时后，自动重传.（重传过程中产生误码）
此时我们看更新后的接收方状态。
接着我们定位到发送方正确重传的第398步。
此时接收方期望的数据和序号是更新后的（2，0)，但是发送方重发的数据一直是（1，1）。因此接收方在接收到数据后，因为接收序号与期望不一致而进行否定确认。
从此发送方一直重发（1,1），而接收方一直对此进行否定确认。数据传输失败。
3。结束语
本文介绍了基于模型检测的协议自动分析工具SPIN的原理和使用。通过对ISPIN在windows7 64位操作系统下的安装和使用,掌握了ISPIN的基本操作。并通过对经典的AB协议在理想状态、信道有误码无丢失和信道有误码有丢失三种不同环境中分别进行建模，并运用SPIN进行自动分析。其中在信道有误码有丢失的情况中，设置了两种错误处理,通过ISPIN验证器进一步观察协议的运行，分析协议存在的问题.从而加深对协议验证技术和形式化描述技术的认识和理解,进一步掌握运用PROMELA语言对协议进行建模，熟悉运用SPIN对网络协议进行分析，提高了实验能力。
联系人：蒋海军；电话：军线：1234;地方:5678；手机：[phone]
邮政编码:654321　地址：江苏省南京市光华路海福巷1号指挥信息系统学院研二队
11