模型检测工具汇总

来源自我的博客

http://www.yingzinanfei.com/2017/02/01/moxingjiancegongjuhuizong/

面向形式化规格语言的模型检测工具

SMV(SymbolicSEO靠我 Model Verifier) 符号模型检测工具

SMV用以检测一个有限状态系统是否满足CTL公式。它的建模方式是以模块为单位，模块可以同步或异步组合，模块描述的基本要素包括非确定性选择，状态转换和并行SEO靠我赋值语句。其模型检测的基本方法是以二叉图表示状态转换关系，以计算不动点的方法检测状态的可达性和其所满足的性质。> http://www.cs.cmu.edu/~modelcheck/smv.html

NSEO靠我uSmv(New Symbolic Model Verifier) 新符号模型检测工具

对SMV重构的一个模型检测工具支持计算树逻辑CTL和线性时序逻辑LTL描述的所有规范整合了以SAT为基础的有界模型检SEO靠我测技术> http://nusmv.fbk.eu/

nuXmv 分析同步有限状态和无限状态系统的新符号模型检测工具

扩展于NuSMV对于有限状态的情形，nuXmv特点是基于SAT算法的有效验证引擎对于无限状SEO靠我态的情形，nuXmv特点是基于SMT的验证技术，与MathSAT5紧密集成> https://nuxmv.fbk.eu/

Uppaal(Uppsala University & Aalborg UnivSEO靠我ersity) 时间自动机的模型检测工具

建模和模拟及验证实时系统的工具> http://www.uppaal.org/

STeP(Stanford Temporal Prover) 斯坦福时间验证器

用模型检SEO靠我测器处理子系统的验证问题用定理证明器将结果汇总处理不限于有限状态系统用推论方式联合模型检测应用于更广泛的系统，包括无限数据域的程序> http://www-step.stanford.edu/

CWB(SEO靠我Concurrency Workbench) 适用于并发系统操作与分析的自动化工具

可以检测系统模型之间的等价关系、FRE-ORDER关系和系统是否能够满足$\mu$-演算的公式建模方法使用CCS语言或LSEO靠我OTOS语言的子集

- 能分析给定程序的状态空间及检测多种语义的等价性和序列性

> http://homepages.inf.ed.ac.uk/perdita/cwb/

VIS(Verification ISEO靠我nteracting with Synthesis) 用于形式验证、综合和模拟有限状态系统的工具

能够综合有限状态系统并验证这些系统的属性> http://vlsi.colorado.edu/~vis/

面SEO靠我向源程序语言的模型检测工具

SPIN(Simple Promela Interpreter) 显式模型检测工具

SPIN用以检测一个有限状态系统是否满足PLTL公式及其他一些性质，包括可达性和循环。建模方式SEO靠我是以进程为单位，进程异步组合，进程描述的基本要素包括赋值语句，条件语句，通讯语句，非确定性选择和循环语句。基本方法是以自动机表示各进程和PLTL公式，以计算这些自动机的组合可接受的语言是否为空的方法检SEO靠我测进程模型是否满足给定的性质。建模语言为PROMELA(PROcess MEta LAnguage)，基于进程结构，有类似C语言的结构> http://spinroot.com/spin/whatisSEO靠我pin.html

BLAST(Berkeley Lazy Abstraction Software Verification Tool) C程序的时序安全属性自动验证工具

基于反例引导的抽象求精框架对C语言SEO靠我程序进行检测采用懒惰抽象(lazy abstraction)技术，有效地提高了效率> http://cseweb.ucsd.edu/~rjhala/blast.html

SLAM C程序模型检测工具

将原CSEO靠我语言程序抽象为布尔程序进程验证工作抽象后的程序仅剩下布尔变量依靠C2bp,Bebop,**Newton**3个工具分别负责完成抽象、检测和抽象求精任务> https://www.microsoft.cSEO靠我om/en-us/research/project/slam/

JPF(Java Path Finder) Java程序验证工具

实现了一个MC-JVM来解决内存分配和垃圾回收等问题> http://babSEO靠我elfish.arc.nasa.gov/trac/jpf

VeriSoft 直接测试C源代码

Eraser 能够检测Java代码Jchecker

C程序模型检测工具

基于谓词抽象理论采用基于谓词抽象的反例引导的抽SEO靠我象求精框架能够针对C程序源码抽象出模型并完备地搜索其状态空间，以此验证程序的安全属性最大限度缩减状态空间

Bandera 并发Java程序的模型检测工具

工具平台基于程序切片技术，将Java程序转换成中间代SEO靠我码后端接口适应多种模型检测器，包括SPIN和SMV> http://bandera.projects.cs.ksu.edu/

Klocwork InsightPro可以检测多种语言类型的多种质量缺陷和安SEO靠我全漏洞

CMC 可以检测C语言程序在执行时OS层级的调度MaceMC

用于检测分布式系统

http://www.macesystems.org/wiki/macemc

Chess用于检测多线程的Windows程SEO靠我序

> https://www.microsoft.com/en-us/research/project/chess-find-and-reproduce-heisenbugs-in-concurrenSEO靠我t-programs/

FDR

> https://www.cs.ox.ac.uk/projects/fdr/

Murphi 一种枚举显示状态的模型检测器，针对C语言

> http://formalverifiSEO靠我cation.cs.utah.edu/Murphi/

MoonWalker 针对.NET应用的模型检测工具

XMC 对JAVA程序中同步操作算法检测

FLAVERS(FLow Analysis for VERiSEO靠我fication of Systems 针对ADA语言的工具

> http://formalverification.cs.utah.edu/Murphi/

Mocha 针对C语言的模型检测工具

> httpsSEO靠我://www.cis.upenn.edu/~mocha/

CBMC 针对C语言/C++的模型检测工具

> http://www.cprover.org/cbmc/

MAGIC(Modular AnalysisSEO靠我 of proGrams In C) 针对C语言的模型检测工具

> http://www.cs.cmu.edu/~chaki/magic/

其他模型检测工具

OFMC 一种用于安全协议的符号模型检测工具CoPSSEO靠我 持久安全性检测器Rational TauF-SoftIMPACTAstree analysis toolSaturnCalystoTerminatorSATABSTerminatormCRL2(micSEO靠我ro Common Representation Language) 并发系统检测工具LTSA(Labeled Transition System Analyzer) 并发系统检测工具 Maude基于逻辑语SEO靠我义的工具ISP MPI程序的检测工具CHIC(Checker for Interface Compatibility) 模块行为兼容性的验证工具MRMC(Markov Reward Model)对离散和连SEO靠我续时间的马尔可夫激励模型UMLChecker UML模型检测工具BACH(Bounded ReachAblity CHecker) 用于分析线性混成自动机有界可达性分析LDPChecker针对正环闭合自动SEO靠我机(Positive Loop-closed Automata)检验线性时段性质QRDChecker针对时段时序逻辑QRDC(Quantified Restrictred Duration CalcuSEO靠我ls)的检验工具KronosHyTechAUTOABSFeaVer3VMCaSpin

其他分类方式

结合模型检测与定理证明

STeP符号模型检测

用有序二叉图OBDDs(Ordered Binary DeciSEO靠我sion Diagrams)描述状态迁移图用布尔逻辑公式描述系统属性定界模型检测技术(bounded model checking)

依赖于布尔可满足性问题(boolean satisfiabilitySEO靠我 problem, SAT)的求解器在限定步数k内，确定系统是否满足性质。若不能确定，则增加k值，重新进行验证

其他分类方式

基于自动机理论

SPIN基于不动点定理

SMV

其他分类方式

针对实时系统的模型检测工SEO靠我具

UPPAAL, Kronos, STeP针对并发系统的模型检测工具

Spin, JPF, Verisoft针对混成系统的模型检测工具

HyTech, HySAT, BACH, LDPChecker

模型检SEO靠我测的步骤：

抽象出系统的数学模型

迁移系统马尔可夫链Kripke结构给出能够描述该系统性质的语言

线性时序逻辑LTL

关心系统的任意一次运行中的状态以及它们之间的关系分支时序逻辑CTL

分叉时序逻辑，用来描述状SEO靠我态的前后关系和分支情况$\mu$-演算

关心系统的动作与状态之间的关系