定理證明器 Coq 模型檢測

---

基於邏輯的形式化驗證方法: 進展及應用

陳鋼1,† 於林宇1,2 裘宗燕3 王穎1
北京大學學報(自然科學版) 2016 年3 月

摘要
近年來, 形式化方法發展很快,一些技術已經產生工業應用。以邏輯系統為主線,分析幾個影響力比較大的形式化驗證技術和驗證工具,以幫助應用工程師選擇並使用形式化工具。主要包括命題演算和時態邏輯方面的SAT、BDD、模型檢測和SMT, 謂詞邏輯方面的ACL2、VDM 方法和B 方法,以及高階邏輯方面的HOL、PVS和COQ。還介紹形式化方法在學術界和工業界的應用情況,最后給出幾個商業化的形式化驗證工具。

關鍵詞 形式化方法; 邏輯系統; 驗證技術

• 形式化方法

  • 定理證明、模型檢測

• Intel: HOL -> FORTE 系統

  • An Industrially Effective Environment for Formal Hardware Verification

• 形式驗證公司

  • JASPER
  • FORMALITY
  • Calypto

1 命題演算和SAT 求解器

• 命題演算(propositional calculus)

  • 描述和證明兩個組合電路的等價性
  • 基本問題: 可滿足性(Satisfiability)和永真性

• 命題演算證明問題兩個重要特點

  • 可判定性, 即可構造出自動化算法, 證明任一命題可滿足性
  • 證明復雜性。命題演算判定問題是一NP完全性問題

• 命題演算自動證明方面兩個重大進展

  • BDD 技術: binary decision diagram
    • Graph-based algorithms for Boolean
      function manipulation
  • SAT 求解器
    • David-Putnam搜索技術(DP 方法)

• 基本SAT 求解技術主要分成兩類

  • 基於沖突分析(conflict analysis)技術
    • Grasp, Sato, Chaff, MiniSat, Berk-Min,Siege 和MaxSAT
  • 基於前向分析(lookahead)技術,
    • Bohm, Posit, Satz,EqSatz, OKsolver, March_dl 和Kcnf等[5]

2 時態邏輯和模型檢測工具

• 3 類特性

  • 安全性(safty properties)
    • 某些狀態(不好的)永遠不會到達;
  • 活性(liveness properties)
    • 某種期待的良好性質遲早會成立
  • 公平性(fairness)
    • 系統提供的各項服務都將有平等機會執行

• 模型檢查[6] -> 時態邏輯

• 模型檢測選擇因素

  • 特性描述語言:
    • 命題邏輯、LTL 或CTL,PSL(property specification language)
  • 模型描述語言
    • C, JAVA,VHDL等源代碼,或Promela
  • 模型檢查工具
    • CBMC
      • Behavioral consistency of C and verilog programs using bounded model checking
    • Cadence SMV
    • UPPAAL

3 SMT 求解器

• SMT[10]
• Ackerman 化方法

組合論么？

4 謂詞邏輯及一階定理證明器

謂詞邏輯重要證明技術: 消解法(resolution),
核心證明規則是一條消解規則:
\(\neg A \vee B, A \vee C \Rightarrow B \vee C\)

4.1 ACL2

• ACL2 [16]: 謂詞邏輯定理證明器

4.2 維也納方法(VDM)

• Z 方法[22]
• Larch[23

4.3 B 方法

• Event-B[26]

5 高階邏輯和證明助手

• 高階邏輯 vs. 類型理論
• LEGO[34]
• COQ

5.1 HOL

5.2 PVS

5.3 COQ

• 四色問題

6 形式化方法的應用方式

6.1 對實際系統或系統部分的驗證

• Contract
  • 基於C#的Spec#[40]
  • 基於Java 的JML[41]

6.2 系統的形式化建模和驗證

6.3 基於形式化方法的系統開發

7 商業化的形式化工具

• Z3
  • Z3 source

8 結語

圖1 概括描述本文涉及的邏輯系統、證明技術和證明工具

• Formality 和JASPER
• COQ

---

Coq

• Coq: 證明輔助工具,提供一個函數式編程語言與和一個基於高階邏輯的推理框架

  • Coq里面命題是類型，程序則證明
  • 數學上,Coq用於驗證四色定理

• seL4: formal verification of an OS kernel

• CompCert

  • 完全證明的C語言編譯器?
    • Certified Software = Program + Proof
  • Formal verification of a realistic compiler

• 其它證明輔助工具

  • Isabelle
  • Twelf
  • Agda

• dependent type

• Ynot: a library for the Coq proof assistant which turns it into a full-fledged environment for writing and verifying imperative programs.

• ATS

  • Hongwei Xi

• 輔酶Q10: 同名不同質

Coq演化

• 1970 年代
  • LISP 語言 -> 一階邏輯證明器SAM
  • System F: 多態 \(\lambda\) 演算
  • ML語言
• 1980年代
  • SOS: 結構化操作語義
  • Objective Caml 語言 -> Coq 證明器的實現語言
  • 構造演算（Calculus of Constructions）
• 1990 年代
• 2000年
  • 圖形界面PCoq

Reference

• Interactive Theorem Proving and Program Development
  • 交互式定理證明與程序開發 Coq歸納構造演算的藝術, 中文版
• Certified Programming with Dependent Types: online
• Software Foundations: online book
  • 經典Coq教材
  • Benjamin C. Pierce

---

定理證明

• Isabelle: 基於高階邏輯的定理輔助證明系統

• PVS: a specification language integrated with support tools and a theorem prover

---

• spin

  • Promela 不支持如浮點數、引用、指針等語言特性

• Java PathFinder

  • Java -> Promela -> SPIN
    • 相當於語法翻譯器，將Java程序轉化為Promela程序，再利用SPIN驗證

• MoonWalker: model checking .NET applications

• ref

  • Reliability analysis in symbolic pathfinder
  • Java多線程程序的測試

---

• NuSMV: 是SMV的重新實現和擴展,且是第一個基於BDDs

  • 計算樹邏輯CTL

• CADP

---

• FDR 3: Failures-Divergence Refinement
  • The CSP refinement checker