前言
SPIN和SMV是课程中介绍了两种特别重要的模型检测工具，本文将介绍两种工具的安装、基本使用，同时使用两种工具来解决农夫过河问题，并对这两种工具进行比较。
一、形式化验证工具的安装
1.1.SPIN的安装
1.1.1下载SPIN可执行文件
进入spin验证工具的官网：http://spinroot.com/spin/whatispin.html
进入安装向导页面，按照指示来进行安装。
Windows 10操作系统可以直接下载二进制文件。
可执行文件链接：http://spinroot.com/spin/Src/pc_spin649.zip
完整文件链接：http://spinroot.com/spin/Src/spin649.tar.gz
或者直接下载：https://pan.baidu.com/s/1mXOpl4kmXTqE46mKqbtz5w提取码：ji9h
下载完毕后解压,切换到spin.exe所在的目录下。
但是，直接跑是不得行的，它会报如下错误：
这是因为SPIN需要将promela语言先转义为C语言，然后再用C语言的编译器例如GCC生成最终的模型检验程序。
因此，还需给Windows 10安装gcc编译器。
1.1.2安装gcc编译器
下载cygwin安装文件。
文件链接：http://www.cygwin.com/setup-x86_64.exe
安装时注意选择安装gcc这个packages。
把路径C:\cygwin64\bin添加到系统的环境变量中。
使环境变量生效：
重新打开powershell,测试一下工具是否可以使用，如果出现如下界面就说明安装成功了。
1.1.3安装SPIN的GUI界面iSpin
自从6.4.9开始,spin的gui界面就改由基于tcltk来实现了。这是因为使用tcltk实现的GUI程序可以具有更好的跨平台移植性。
首先需要安装tclck.下载tcltk安装包,下载链接：https://bitbucket.org/tombert/tcltk/downloads/tcltk86-8.6.8-10.tcl86.Win7.x86_64.tgz
把文件解压后，将文件的bin路径添加到环境变量，并使环境变量生效。
然后切换到刚刚spin649所在的目标，输入：wish ispin.tcl，打开图形界面。
图形化界面视图：
运行一个Example测试一下。
输入：
1 init {
2 printf("passed first test!\n")
3 }
发现会报错：
这是因为刚刚没有把spin.exe所在的目录添加到环境变量中。现在把spin.exe所在目录添加至环境变量，并使环境变量生效，从新打开ispin图形化界面。
运行结果：
还是要报错，查询资料后发现需要做如下修改。
把刚刚安装的cygwin for 64bit,改成cygwin for 32 bit.这是因为spin只会生成32位的pan.c代码。
Cygwin for 32bit下载地址：https://cygwin.com/setup-x86.exe,安装过程同1.2所示。安装完毕后。
再运行Verification:
发现就是成功的了。
1.2.NuSMV的安装
1.2.1NuSMV下载
在http://nusmv.fbk.eu/bin/bin_download2-v2.cgi 页面下载合适的二进制可运行版本即可。在本报告中使用的是http://nusmv.fbk.eu/distrib/NuSMV-2.6.0-win64.tar.gz 文件。
解压后，即可得到具有如下目录的文件夹：
在bin目录下有可执行文件nusmv.exe，直接在命令行运行即可。
当然，为了方便起见，也可以将NuSMV.exe所在的目录添加到系统的环境变量中，这样就可以在系统的任意工作目录使用NuSMV。
1.2.2NuSMV可运行测试
可以测试一下看是否NuSMV.exe是否可用。
可以发现是可以运行的。
二、使用SPIN和SMV解决农夫过河问题
2.1问题描述
一个人带着狼、山羊和白菜在一条河的左岸，有一条船，大小正好能装下这个人和其它三者之一，人和他的随行物都要带过岸，但他每次只能带一样东西摆渡过河。如人将狼和羊留在同一岸，无人照顾，那么狼会把羊吃掉。同样，如羊和白菜在同一岸，无人照顾，那么羊会吃了白菜。
2.2农夫过河问题的有限状态机
其中MGCW-Empty表示初始状态。“—”左边的符号表示对应的符号在左岸。“—”右边的服务表述对应的符号在右岸。
M表示人，G表示羊goat,C表示白菜Cabbage,W表示狼wolf.
箭头表示表示每次在船上运输的物品的种类。
2.3使用NuSMV解决农夫过河问题
2.3.1编码实现
MODULE main
VAR
ferrymen:boolean;
goat:boolean;
wolf:boolean;
cabbage:boolean;
ship:{goat_man,wolf_man,cabbage_man,empty,man};
--ship 表示船上装着是什么
ASSIGN
init(ferrymen):=FALSE; --人在左边
init(goat):=FALSE; --羊在左边
init(wolf):=FALSE; --狼在左边
init(cabbage):=FALSE; --白菜在左边
init(ship):=empty; --船上为空
--初始化的时候,全部在河岸的左边FALSE
ASSIGN
next(ship):=
case
ferrymen=TRUE&ferrymen=goat & goat=wolf & goat=cabbage :empty; --全部已经过河,不再运输
ferrymen=FALSE & goat=FALSE & wolf=FALSE & cabbage=FALSE : {goat_man}; --表示状态1的转移关系
ferrymen=TRUE&goat=TRUE & cabbage=FALSE & wolf=FALSE :{goat_man,man}; --表示状态2的转移关系
ferrymen=FALSE & cabbage=FALSE&wolf=FALSE&goat=TRUE : {man,wolf_man,cabbage_man}; --表示状态3的转移关系
ferrymen=TRUE & cabbage=FALSE & wolf=TRUE&goat=TRUE : {goat_man,wolf_man}; --表示状态4的转移关系
ferrymen=FALSE & cabbage=FALSE & wolf=TRUE&goat=FALSE : {goat_man,cabbage_man}; --表示状态5的转移关系
ferrymen=TRUE & cabbage=TRUE & wolf=TRUE&goat=FALSE : {man,cabbage_man,wolf_man}; --状态6的转移关系
ferrymen=FALSE & cabbage=TRUE & wolf=TRUE&goat=FALSE : {goat_man,man}; --状态7的转移关系
ferrymen=TRUE & cabbage=TRUE & wolf=FALSE&goat=TRUE : {cabbage_man,goat_man}; --状态9的转移关系
ferrymen=FALSE & cabbage=TRUE & wolf=FALSE&goat=FALSE : {wolf_man,goat_man}; --状态10的转移关系
TRUE: empty;
esac;
next(goat):=
case
(next(ship)=goat_man)& ferrymen=goat: next(ferrymen); --如果运输的是人和羊,那么人和羊都换到另外一边
TRUE : goat;
esac;
next(wolf):=
case
(next(ship)=wolf_man) & ferrymen=wolf: next(ferrymen); --如果运输的是人和狼,那么人和狼都换到另外一边
TRUE :wolf;
esac;
next(cabbage):=
case
(next(ship)=cabbage_man)& ferrymen=cabbage: next(ferrymen); --如果运输的人和白菜,那么人和白菜都转移
TRUE: cabbage;
esac;
next(ferrymen):=
case
(ship=empty): ferrymen;
TRUE:!ferrymen ; --每次都需要人的陪同
esac;
--每次都要人陪同
CTLSPEC
!E [( ((goat=wolf)-> (goat=ferrymen)) & ((goat=cabbage)->(goat=ferrymen)))
U ((cabbage=TRUE)& (goat=TRUE) & (wolf=TRUE) &(ferrymen=TRUE))]
### 2.3.2实现说明
ferrymen,goat,wolf,cabbage都是boolean类型的变量，分别表示人、羊、狼、白菜是否在河的右边。当他们的值为FALSE的时候，说明他们在左边，否则在右边。
ship表示每次船上运输的东西，它的取值为goat_man（同时运人和羊）、wolf_man(同时运人和狼)、cabbage_man(同时运人和白菜)、man(只运人)、empty(什么都不运)。
初始化时设置所有的变量的初始值，对应于状态机的初始状态。
写出转移过程：
2.3.3安全过河的条件
CTLSPEC
E [( ((goat=wolf)-> (goat=ferrymen)) & ((goat=cabbage)->(goat=ferrymen)))
U ((cabbage=TRUE)& (goat=TRUE) & (wolf=TRUE) &(ferrymen=TRUE))]
2.3.4模型检测结果
使用NuSMV运行上面的农夫过河实现，得到结果如下：
说明是的确是存在这么一条运输方法的。
2.3.5过河路径
因为NuSMV只会举出不符合所需要性质的反例，因此为了得到一条运输路径，可以写出上述的非，表示不存在这么一条路径···，然后NuSMV就会找出一个反例，而这个反例就是我们所需要的运输方法。
检验的性质为：
CTLSPEC
!E [( ((goat=wolf)-> (goat=ferrymen)) & ((goat=cabbage)->(goat=ferrymen)))
U ((cabbage=TRUE)& (goat=TRUE) & (wolf=TRUE) &(ferrymen=TRUE))]
模型验证结果：
这个结果显示的运输路径如下：
1. 船上先运输羊和人，这样goat=TRUE,ferrymen=TRUE
2. 人在单独过河，这样ferrymen=FALSE
3. 人和狼过河，这样ferrymen=TRUE,goat=TRUE,wolf=TRUE.
4. 人把羊带过河，这样ferrymen=FALSE,goat=FALSE
5. 人把白菜带过河，这样ferrymen=TRUE,cabbage=TRUE
6. 在再单独过河，这样ferrymen=FALSE
7. 最后，人带着羊一起过河。
2.4使用SPIN解决农夫过河问题
2.4.1编码实现
mtype={original_side,destination_side}
mtype ferryman=original_side,
cabbage=original_side,
goat=original_side,
wolf=original_side;
inline swap_side(loc)
{
if
:: loc==original_side -> loc =destination_side
:: else -> loc =original_side
fi
}
inline carry(object)
{
atomic{
swap_side(ferryman);
swap_side(object);
}
}
inline carry_nothing()
{
atomic
{
swap_side(ferryman);
}
}
proctype cross_river()
{
do
:: carry_nothing()
:: ferryman==goat -> carry(goat)
:: ferryman==wolf -> carry(wolf)
:: ferryman==cabbage-> carry(cabbage)
od
}
init
{
run cross_river();
}
#define GOAL ((ferryman==destination_side) && (wolf==destination_side) && (goat==destination_side) && (cabbage==destination_side))
#define COND ((wolf==goat && ferryman != wolf)||(goat==cabbage && ferryman==goat))
ltl nice {((!COND) U GOAL)}
2.4.2实现说明
首先通过mtype定义河的两岸：mtype={original_side,destination_side}
接着将农夫、白菜、羊、狼初始化在原岸边：
mtype ferryman=original_side,
cabbage=original_side,
goat=original_side,
wolf=original_side;
接下来实现swap_side部分，这是一个inline函数，它不是一个进程，但是可以传递参数。它表示把loc从一边运到另外一边。
接着实现携带物品过河的函数carry(object).注意里面是一个atomic语句。之所以用atomic是为了表达携带物品过河的动作要么人和物品一起过河，要么都不过河。
carry_nothing用于表示人空手过河。
cross_river进程才是关键。
proctype cross_river()
{
do
:: carry_nothing()
:: ferrymangoat -> carry(goat)
:: ferrymanwolf -> carry(wolf)
:: ferryman==cabbage-> carry(cabbage)
od
}
过河一共存在四种情况：要么人空手过河、要么人现在和羊在一边，那么接下来带着羊过河、要么带着狼过河、要么带着白菜过河。
SPIN里面的循环语句：do里面是从其中四条语句选一条满足条件的执行；如果有多条语句同时可执行，那么随机选一条。
2.4.3安全过河条件
#define GOAL ((ferryman==destination_side) && (wolf==destination_side) && (goat==destination_side) && (cabbage==destination_side))
#define COND ((wolf==goat && ferryman != wolf)||(goat==cabbage && ferryman==goat))
ltl nice {((!COND) U GOAL)}
SPIN里面的性质都是使用宏来定义的。GOAL表示最终的目标，人和羊和白菜和狼都过河。
COND表示需要满足的条件：如果狼和羊在一起，那么人就必须得和他们在一起；同时羊和白菜在一起，那么人必须也得羊在一起。
ltl nice xxx则是用ltl的语法写了这个约束。
2.4.4模型检测结果
我们使用iSPIN图形化界面来检测模型。SPIN会在性质前面自动添加一个Never来寻找一条不满足的路径,表示不存在那么一条路径使用到达目标前满足我们写的安全条件。可以看到，在Verification 部分，SPIN检测到了一条可行路径。
然后我们在iSPIN的Simulation/Replay页面可以看到整个的路径。
2.4.5过河路径
SPIN输出的过河路径比较长，主要是SPIN会有很多的农夫不携带任何物品而在河的两岸空转。我们把这些空转的路径给人工过滤掉即可得到一条简化的路径。
1. 船上先运输羊和人，这样goat=destination_side,ferrymen=destination_side
2. 人在单独过河，这样ferrymen=original_side
3. 人和菜带过河，这样ferrymen=destination_side,goat=destination_side,
cabbage=destination_side.
4. 人把羊带过河，这样ferrymen=original_side,goat=original_side;
5. 人把狼带过河，这样ferrymen=destination_side,wolf=destination_side
6. 人再单独过河，这样ferrymen=original_side
7. 最后，人带着羊一起过河。然后就全部安全过河了。
三、总结
3.1SPIN与SMV的比较
本人在做课后作业“农夫过河问题”使用的SMV工具来完成的。SPIN和SMV都是基于有限状态机来做形式化验证的。但是在使用过程中，个人感觉SPIN会比SMV具有更强的模型表达能力。因为SPIN是使用Promela语言来描述模型的，它可以很方便、自然的表达系统里面的各个并发进程。而SMV则是着重把状态机的状态转移表达出来，它在表达多个系统的同步转移的时候是需要进行一定的构造和转化的，它不想SPIN那样自然。
在输出结果上，SMV提供的错误反馈是一系列在执行路径上的各个状态的变量值的额序列，这一点非常类似于文本性的输出。这种过于简单的输出，使得寻找错误的过程变得非常困难和低效。而SPIN提供的错误反馈是整个协议执行的轨迹图，并且轨迹图直接编辑了发生错误（Assert失败）的具体行数。这使的分析变得更加便利和直观。例如2.4.4和2.3.4两个工具在输出过河路径的时候，SPIN就便于调试，它可以最终系统每个状态各个变量的值；而SMV则只是把最终的结果输出出来。
而且SPIN是具有图形化界面iSPIN的，因此其对用户的友好程度更佳，但从实际的使用体验来说SPIN的图形化界面奇丑无比，还不如输入命令行来的快。
SPIN相比SMV最大的优势在于：SPIN可以很方便的表达原子操作、不同实体之间交互的语义、同时SPIN也天生的对C语言支持很大。例如，在使用SMV不支持原子操作这种原语。于是在用SMV表达人携带着白菜过河时，写出的语句就不是特别直观，需要在case语句中使用两个next来表达这个原子语义。
next(cabbage):=
case
(next(ship)=cabbage_man)& ferrymen=cabbage: next(ferrymen); --如果运输的人和白菜,那么人和白菜都转移
TRUE: cabbage;
esac;
然后SPIN是不支持CTL的，这是其不如SMV的地方。有些性质使用CTL可以很好的表达，例如存在一条路径，使得这条路径所有的节点都满足···。LTL在表达这种语义就不是特别方便了。