模型檢測工具匯總

面向形式化規格語言的模型檢測工具

SMV(Symbolic Model Verifier) 符號模型檢測工具

• SMV用以檢測一個有限狀態系統是否滿足CTL公式。
• 它的建模方式是以模塊為單位，模塊可以同步或異步組合，模塊描述的基本要素包括非確定性選擇，狀態轉換和并行賦值語句。
• 其模型檢測的基本方法是以二叉圖表示狀態轉換關系，以計算不動點的方法檢測狀態的可達性和其所滿足的性質。
• > http://www.cs.cmu.edu/~modelcheck/smv.html

NuSmv(New Symbolic Model Verifier) 新符號模型檢測工具

• 對SMV重構的一個模型檢測工具
• 支持計算樹邏輯CTL和線性時序邏輯LTL描述的所有規范
• 整合了以SAT為基礎的有界模型檢測技術
• > http://nusmv.fbk.eu/

nuXmv 分析同步有限狀態和無限狀態系統的新符號模型檢測工具

• 擴展于NuSMV
• 對于有限狀態的情形，nuXmv特點是基于SAT算法的有效驗證引擎
• 對于無限狀態的情形，nuXmv特點是基于SMT的驗證技術，與MathSAT5緊密集成
• > https://nuxmv.fbk.eu/

Uppaal(Uppsala University & Aalborg University) 時間自動機的模型檢測工具

• 建模和模擬及驗證實時系統的工具
• > http://www.uppaal.org/

STeP(Stanford Temporal Prover) 斯坦福時間驗證器

• 用模型檢測器處理子系統的驗證問題
• 用定理證明器將結果匯總處理
• 不限于有限狀態系統
• 用推論方式聯合模型檢測應用于更廣泛的系統，包括無限數據域的程序
• > http://www-step.stanford.edu/

CWB(Concurrency Workbench) 適用于并發系統操作與分析的自動化工具

• 可以檢測系統模型之間的等價關系、FRE-ORDER關系和系統是否能夠滿足$\mu$-演算的公式
• 建模方法使用CCS語言或LOTOS語言的子集

- 能分析給定程序的狀態空間及檢測多種語義的等價性和序列性

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

VIS(Verification Interacting with Synthesis) 用于形式驗證、綜合和模擬有限狀態系統的工具

• 能夠綜合有限狀態系統并驗證這些系統的屬性
• > http://vlsi.colorado.edu/~vis/

面向源程序語言的模型檢測工具

SPIN(Simple Promela Interpreter) 顯式模型檢測工具

• SPIN用以檢測一個有限狀態系統是否滿足PLTL公式及其他一些性質，包括可達性和循環。
• 建模方式是以進程為單位，進程異步組合，進程描述的基本要素包括賦值語句，條件語句，通訊語句，非確定性選擇和循環語句。
• 基本方法是以自動機表示各進程和PLTL公式，以計算這些自動機的組合可接受的語言是否為空的方法檢測進程模型是否滿足給定的性質。
• 建模語言為PROMELA(PROcess MEta LAnguage)，基于進程結構，有類似C語言的結構
• > http://spinroot.com/spin/whatispin.html

BLAST(Berkeley Lazy Abstraction Software Verification Tool) C程序的時序安全屬性自動驗證工具

• 基于反例引導的抽象求精框架對C語言程序進行檢測
• 采用懶惰抽象(lazy abstraction)技術，有效地提高了效率
• > http://cseweb.ucsd.edu/~rjhala/blast.html

SLAM C程序模型檢測工具

• 將原C語言程序抽象為布爾程序進程驗證工作
• 抽象后的程序僅剩下布爾變量
• 依靠C2bp,Bebop,**Newton**3個工具分別負責完成抽象、檢測和抽象求精任務
• > https://www.microsoft.com/en-us/research/project/slam/

JPF(Java Path Finder) Java程序驗證工具

• 實現了一個MC-JVM來解決內存分配和垃圾回收等問題
• > http://babelfish.arc.nasa.gov/trac/jpf

VeriSoft 直接測試C源代碼

• 基于謂詞抽象理論
• 采用基于謂詞抽象的反例引導的抽象求精框架
• 能夠針對C程序源碼抽象出模型并完備地搜索其狀態空間，以此驗證程序的安全屬性
• 最大限度縮減狀態空間

Bandera 并發Java程序的模型檢測工具

• 工具平臺
• 基于程序切片技術，將Java程序轉換成中間代碼
• 后端接口適應多種模型檢測器，包括SPIN和SMV
• > http://bandera.projects.cs.ksu.edu/

Klocwork InsightPro 可以檢測多種語言類型的多種質量缺陷和安全漏洞

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

Chess 用于檢測多線程的Windows程序

• > https://www.microsoft.com/en-us/research/project/chess-find-and-reproduce-heisenbugs-in-concurrent-programs/

FDR

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

Murphi 一種枚舉顯示狀態的模型檢測器，針對C語言

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

MoonWalker 針對.NET應用的模型檢測工具

FLAVERS(FLow Analysis for VERification of Systems 針對ADA語言的工具

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

Mocha 針對C語言的模型檢測工具

• > https://www.cis.upenn.edu/~mocha/

CBMC 針對C語言/C++的模型檢測工具

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

MAGIC(Modular Analysis of proGrams In C) 針對C語言的模型檢測工具

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

其他模型檢測工具

其他分類方式

• 結合模型檢測與定理證明
  
  • STeP
• 符號模型檢測
  
  • 用有序二叉圖OBDDs(Ordered Binary Decision Diagrams)描述狀態遷移圖
  • 用布爾邏輯公式描述系統屬性
• 定界模型檢測技術(bounded model checking)
  
  • 依賴于布爾可滿足性問題(boolean satisfiability problem, SAT)的求解器
  • 在限定步數k內，確定系統是否滿足性質。
  • 若不能確定，則增加k值，重新進行驗證

其他分類方式

• 基于自動機理論
  
  • SPIN
• 基于不動點定理
  
  • SMV

其他分類方式

• 針對實時系統的模型檢測工具
  
  • UPPAAL, Kronos, STeP
• 針對并發系統的模型檢測工具
  
  • Spin, JPF, Verisoft
• 針對混成系統的模型檢測工具
  
  • HyTech, HySAT, BACH, LDPChecker

模型檢測的步驟：

• 遷移系統
• 馬爾可夫鏈
• Kripke結構

• 線性時序邏輯LTL
  
  • 關心系統的任意一次運行中的狀態以及它們之間的關系
• 分支時序邏輯CTL
  
  • 分叉時序邏輯，用來描述狀態的前后關系和分支情況
• $\mu$-演算
  
  • 關心系統的動作與狀態之間的關系