NuSMV使用教程.docx
NuSMV使用教程摘要：本教程简要介绍模型检测(MOdelCheCking)技术，并提供对模型检测工具NUSMV的相关教程，包括安装方式、其接受的输入语言格式及使用实例。一、简要介绍模型检测(MOdelCheCking)是一种验证技术，它以蛮力搜索的方式遍历系统所有可能的状态。通过这种方式，可以证明给定的系统模型确实满足某个特性或者违反某个特性。目前模型检测最大的挑战是状态空间爆炸，最新的模型检测工具可以通过显式的状态空间枚举处理大约108到109个状态的状态空间，如果使用巧妙构造的算法和特定的数据结构，可以针对特定问题处理更大的状态空间(IO?。个甚至更多状态)。模型检测最大的优势是能够毫无遗漏的发现系统所有的错误，比如模拟、仿真和测试未发现的细微错误。图1模型检测示意图2001年，基于SMV(SymbolicModelVerifier),CamegieMellonUniVerSity(CMU)和IStitUtoperlaRicercaScientificaeTecholgica(IRST)联合开发出模型验证器NuSMV,它主要是针对SMV2.4.4版本的重新实现和扩展，重新定义了软件架构并加入了一些新特性。NuSMV目前已发展到2.6.0版本。具体来说,NuSMV从三个方面扩展了SMV：功能上，除了可以验证用CTL描述的规范外,还可以验证用LTL描述的规范；不仅实现了经典的基于BDD的符号模型检测技术外，还整合了基于SAT的有界模型验证技术(BMC)；提供了一个类似于UniX的Shen的接口，方便用户使用。>相对于SMV,NUSMV定义了一个良好的软件系统架构，实现也更加模块化和开放，容易删除、替换或添加模块。例如，可以使用商用的ZChaff包提供更加高效的有界模型验证技术。>NuSMV源码的注释、文档化更加完整，比SMV更加容易读和便于修改。这归因于NuSMV的一个目标是提供一个模型检测的通用平台，所以在编码上考虑到未来的扩展和修改。可用资源：1. NUSMV工具网址：2. NUSMV用户手册:3. NUSMV官方教程：二、NuSMV的安装推荐第2种，方便快捷！1、从源码安装(仅展示GNU/IJnUX系统)，系统要求：GNU/Linux,比如Ubuntuo(以下例程基于Ubuntu20.04LTSamd64)# 安装依赖sudoaptinstallgccg+flexbisoncmaketargziplibxml2libreadline6-devdoxygentexlivetexmaker# 在Ubuntu上进行编译wgettarzxvfNuSMV-2.6.0.cdNuSMV-2.6.0NuSMVmkdirbuildCdbuildcmake.geditcode/nusmv/shell/cmd/cmdHelp.c# 修改58行为:wintCommancLnumber;"geditdoc/prog-man/cmake_# 删除49行内容：7html”geditCUdd-2.4.1.lutilPiPefOrk.c# 修改43行为:"#if(defined_linux_)(defined_hpux)(defined_osf_)H(definedJBMR2)(defined_SVR4)(defined_CYGWIN32_)(defined_MINGW32_)Wgedit././MiniSat/MiniSat_v37dc6c6_# 修改679行为："+cxte"C"voidMiniSaJDelete(MiniSaJPtrms)”gedit././NuSMV/cmake/combine_# 修改41行为:"forkeyinsorted(d,reverse=True):Mmakesudomakeinstall使用方式：NuSMVusrlocalsharenusmvexamplessmv-dist注：上述安装过程将NUSMV安装至目录usrlocal中，其中示例文件目录为usrlocalShare/nusmv/examples。2、下载二进制文件、解压运行即可。1) GNU/Linux系统，比如Ubuntu：# GNU/Linuxlibc6(686)32-bitwgettarzxvfNuSMV-2.6.gzsudocp-RNuSMV-2.6.0-Linux*usrlocal# GNU/Linuxlibc6(x86)64-bitwgettarzxvfNuSMV-2.6.gzsudocp-RNuSMV-2.6.0-Linux*usrlocal使用方式：NuSMVusrlocalsharenusmvexamplessmv-dist注：上述安装过程将NUSMV安装至目录usrlocal中，其中示例文件目录为usrlocalShare/nusmv/examples。2) WindOWS系统：# Windowsarchive32-bit(586)# 下载地址# 解压缩包，比如至C:ProgramFiles(x86)NuSMV-2.6.0-win32# 然后配置PATH,编辑Path,添加1C:ProgramFiles(x86)NuSMV-2.6.0win32bin# 使用方式，打开Cmd键入：NuSMV"C:ProgramFiles(x86)NuSMV-2.6.0-win32sharenusmvexamplessmv-dist"注：上述安装过程将NuSMV安装至目录C:ProgramFiles(x86)NuSMV-2.6.0-win32中，其中示例文件目录为C:ProgramFiles(x86)NuSMV-2.6.0-win32sharenusmvexampleSo# Windowsarchive64-bit(x86)# 下载地址# 解压缩包，比如至C:ProgramFiles(x86)NuSMV-2.6.0-win64# 然后配置PATH,编辑Path,添加C:ProgramFiles(x86)NuSMV-260-win64bin# 使用方式，打开cmd键入：NuSMV"C:ProgramFiles(x86)NuSMV-2.6.0-win64sharenusmvexampIessmv-dist"注：上述安装过程将NuSMV安装至目录C:ProgramFiles(x86)NuSMV-2.6.0-win64中，其中示例文件目录为C:ProgramFiles(x86)NuSMV-2.6.0-win64sharenusmvexampleSo3) MacOS系统：# MacOSXDarwin(x86)64-bit# 下载地址# 其余步骤请参考1)三、实例介绍NuSMV用smv输入语言(规定的一种文本格式)来描述Kripke结构和待验证的规范。在NUSMV中KriPke结构常称为FiniteStateMaChine(FSM)0其输入语言中，表达式和语句类似于C语言。NUSMV有两个重要的表达式：init表达式和next表达式。> init表达式用于描述初始状态；> next表达式用于描述转移关系。其程序(比如)常被称为SmV程序，由模块(MODULE)构成。模块由模块名和模块定义组成，模块定义又由形参(Parameter)和主体（body）部分组成。模块主体部分分为三类：Variables部分、Constraint部分和Specification部分。> Variables部分用于描述Kripke模型的状态集；> Constraint部分用于描述Kripke模型的转移关系和对模型的一些限制；> Specification部分用来描述待验证规范。另smv程序至少要有一个称为main的模块，且main模块不能有形参。可以使用多个模块描述FSM,然后组合成一个整体的FSM。一个典型的smv程序的结构如下：MODULEmain至少要有一个main模块，为系统建模VAR状态变量声明ASSIGN.初始状态和转移关系的声明SPEc（或LTLSPEC、CTLSPEC）规范定义，可选使用CTL或LTL描述特验证的系统规范Me）DULESUbmodUIe各个子模块的定义，可选.同main模快1) VariabIeS部分有两大类：> StateVaribles（状态的赋值表示具体的某个状态）；> InputVaribles（通过标记关系来表示状态）。分别以关键字VAR或IVAR表示。Variables的类型仅为boolean>integer>enum>word>array以及Set类型。2) COnStraintS的种类有assign、trans>init>invar>fairness等，分别以关键字ASSIGN、TRANS>INlT、INVAR>FAlRNESS表示。为了更加方便地描述FSM,NuSMV还引入了DEFINEoDEFINE定义的符号的可看成是一个宏。3) Specification部分可以使用CTL公式，也可以使用LTL公式。以下为源程序的示例：MODULEmainVARbit:counter_cell(TRUE);bitl:counter_cell(_out);bit2:counter_cell(_out);SPECAGAF_outMODULEcounter_cell(carryjn)VARvalue:boolean;ASSIGNinit(value):=FALSE;next(value):=valuexorcarryjn;DEFINEcarry_out:=value&carryjn;该程序为3位二进制计数器电路的模型。以下简要分析：由main模块可知，调用了3次counter_cell模块，所以整体模块拥有3个boolean变量,。ASSlGN语句中的init指定初始状态为(，)=(O,0,0)oASSlGN语句中的next指定下一状态：>=TRUE=> =OUt=(&TRUE)=；> =一OUt=(&_out)=(&(&TRUE)=(&)。由上述转移关系可知，(,)：(0,0,0)(0,0,1)(0,1,0)(1,1,1)(0,0,0)o因此该程序为3位二进制计数器电路的模型。要验证的规范为CTL规范：AGAF_out,即AG(AF&&),该规范含义：对CTL计算树中所有路径，路径中所有节点，该节点的所有后续路径，路径中存在一个节点使得该节点满足=TRUEo从计数器的模型中，容易想象该规范是满足的(计数器从OoO一直增到111,再变为OO0,以此循环下去)。事实上，含有多个模块程序可以转化为仅含一个main模块的程序。以下为示例：MODULEmainVARa: SubModulel;b: subModule2;c: 10.20;MODULESubModulelVARvalue:boolean;b:start,end;MODULEsubModule2VARvalue:0.7;ASSIGNnext(value):=2;MODULEmainVARa.value:boolean;a.b:start,end;/b.value:0.7;c:10.20;ASSIGNnext(b.value):=2;注：上述程序中b.vake表示07之间的整数，包含0、7。更多示例查看sharenusmvexamples目录。
