第1章緒論

1.1形式化方法的發展歷程

1.2形式化方法的基本內容

1.2.1繫統建模

1.2.2形式規約

1.2.3形式驗證

1.3本章小結

習題1

第2章程序正確性證明

2.1Floyd前後斷言法

2.1.1基本概念

2.1.2證明方法

2.1.3應用舉例

2.2Hoare公理化方法

2.2.1基本概念

2.2.2證明方法

2.2.3應用舉例

2.3Dijkstra弱前置條件方法

2.3.1基本概念

2.3.2證明方法

2.3.3應用舉例

2.4本章小結

習題2

上篇繫 統 建 模
第3章遷移繫統

3.1基本概念

3.1.1形式定義

3.1.2遷移圖

3.1.3計算

3.2應用舉例

3.2.1時序電路

3.2.2數據依賴繫統

3.2.3並發和交錯

3.3本章小結

習題3

第4章自動機

4.1有窮自動機

4.1.1有窮狀態繫統

4.1.2形式定義

4.1.3判定算法

4.2Büchi自動機

4.2.1ω有窮自動機簡介

4.2.2Büchi自動機

4.2.3應用舉例

4.3本章小結

習題4

第5章Petri網

5.1庫所/變遷Petri網

5.1.1基本概念

5.1.2基本性質

5.1.3分析方法

5.1.4應用舉例

5.2謂詞/變遷Petri網

5.2.1基本概念

5.2.2應用舉例

5.3著色Petri網

5.3.1基本概念

5.3.2應用舉例

5.4本章小結

習題5

中篇形 式 規 約
第6章時序邏輯

6.1線性時序邏輯

6.1.1LTL語法

6.1.2LTL語義

6.1.3應用舉例

6.2分支時序邏輯

6.2.1CTL語法

6.2.2CTL語義

6.2.3應用舉例

6.3區間時序邏輯簡介

6.4本章小結

習題6

第7章並發繫統屬性

7.1基本概念

7.2安全性

7.2.1形式定義

7.2.2形式描述

7.2.3應用舉例

7.3活性

7.3.1形式定義

7.3.2形式描述

7.3.3應用舉例

7.4本章小結

習題7

下篇形 式 驗 證
第8章定理證明

8.1時序邏輯演繹驗證方法

8.1.1PLTL邏輯繫統

8.1.2MannaPnueli演繹規則方法

8.1.3驗證工具STeP及應用

8.2自動定理證明方法

8.2.1SAT求解算法

8.2.2SMT求解技術

8.2.3ATP方法小結

8.3交互式定理證明方法

8.3.1主要證明輔助工具簡介

8.3.2應用舉例

8.3.3ITP方法小結

8.4本章小結

習題8

第9章模型檢測

9.1基本概念

9.2模型檢測算法

9.2.1CTL模型檢測算法

9.2.2LTL模型檢測算法

9.3模型檢測工具及應用

9.3.1驗證工具SPIN

9.3.2應用舉例

9.4本章小結

習題9

第10章符號模型檢測

10.1二叉判定圖

10.1.1基本概念

10.1.2約簡方法

10.1.3Apply操作及應用

10.2CTL符號模型檢測

10.2.1基本方法

10.2.2驗證工具SMV

10.2.3應用舉例

10.3LTL符號模型檢測簡介

10.4本章小結

習題10

第11章概率模型檢測

11.1概率模型

11.1.1離散時間馬爾可夫鏈

11.1.2馬爾可夫決策過程

11.1.3連續時間馬爾可夫鏈

11.2概率時序邏輯

11.2.1概率計算樹邏輯

11.2.2連續隨機邏輯

11.3概率模型檢測工具及應用

11.3.1驗證工具PRISM

11.3.2應用舉例

11.4本章小結

習題11

第12章實時與混成繫統驗證

12.1時間自動機

12.1.1語法

12.1.2語義

12.2實時邏輯

12.2.1時間計算樹邏輯

12.2.2度量區間時序邏輯

12.3實時繫統模型檢測

12.3.1基本方法

12.3.2驗證工具UPPAAL

12.3.3應用舉例

12.4混成繫統驗證簡介

12.4.1混成自動機

12.4.2微分動態邏輯

12.4.3混成繫統模型檢測

12.5本章小結

習題12

參考文獻

近年來，形式化方法的一個重要內容——基於定理證明的形式驗證方法取得了較大進展和突破。一方面，隨著自動證明理論的發展和計算機處理器能力的大幅增強，基於自動定理證明器的自動驗證能力大幅提升，如微軟公司開發的SMT求解器Z3已成為目前使用廣泛的自動定理證明器； 另一方面，基於人機交互的半自動證明在可驗證的繫統軟件上取得顯著突破，如分別在交互式定理證明器Coq和Isabelle/HOL的支持下，INRIA對C語言編譯器CompCert的驗證及NICTA對操作繫統微內核seL4的驗證等。

本次修訂除更正第1版的一些文字及印刷錯誤和敘述不當之處外，主要修訂第8章及與之關聯的部分章節內容，重點闡述了一些典型的定理證明方法、工具和應用。此外，還補充介紹了我國科學家在形式化方法領域的部分開創性研究工作。

本書修訂工作得到江蘇省高等學校重點教材立項建設、江蘇高校優勢學科建設工程項目資助和江蘇省計算機學會立項資助，以及蘇州大學教務處和計算機科學與技術學院的關心和支持，中國科學院軟件研究所晏榮傑副研究員對本書修訂提出了寶貴的建議，清華大學出版社安妮編輯為本書再版做了大量工作，在此一並表示誠摯的感謝。

張廣泉
2023年1月於蘇州大學天賜莊校區

第1版前言

軟件產業是信息產業的核心，是國家信息化的基礎和支撐。軟件是工業4.0和中國制造2025的使能和驅動。為推進產業結構優化升級，加快培養軟件人纔的步伐，近年來大力發展高校軟件工程教育，軟件工程已從初的計算機科學與技術的一個學科方向調整為包括軟件工程理論與方法、軟件工程技術、軟件服務工程和領域軟件工程等學科方向的、獨立的一級學科。軟件工程理論與方法是軟件工程一級學科的基礎，作為其核心內容之一，形式化方法是指有嚴格數學基礎的軟件和繫統開發方法，支持軟件與繫統的規約、設計、驗證與演化等活動。隨著軟件可信需求的不斷增長，形式化方法的重要性和關注度日益提高。

形式化方法相關的教學工作已經得到歐美國家高等學校的重視和推廣，知識體繫和課程教學內容日趨完善。而目前國內高校關於形式化方法教育還相對薄弱，主要因素之一是缺乏比較全面、繫統介紹形式化理論、方法和應用的教材。

本書是在學習、總結形式化方法領域國內外相關文獻的基礎上，結合作者多年從事形式化方法教學和科研的實踐撰寫而成的，本書具有以下幾個特點： 

（1） 通過詳細分析和梳理，提煉出形式化方法核心、本質的原理、方法和技術，其中自動機和時序邏輯是貫穿全書內容的兩大重要基礎。

（2） 重點闡述以模型檢測為主要內容的形式化驗證方法，使學生在有限的學時範圍內，能有效地掌握形式化方法自動化部分的核心內容。

（3） 注重實踐與應用，詳細介紹SPIN、UPPAAL和PRISM等典型的形式化驗證工具的使用方法，結合實例分析，達到理論學習與實際應用的有機結合。

全書共12章。其中第1章概述形式化方法的發展歷程和基本內容，第2章介紹形式化方法發展早期的經典內容，即串行程序的正確性證明。其餘部分針對並發繫統，分為上、中、下三篇闡述形式化建模、規約和驗證方法。其中： 

上篇（第3～5章）為繫統建模篇，主要介紹三個典型的並發繫統計算模型。第3章介紹基於狀態遷移的計算模型——遷移繫統，第4章介紹描述有窮狀態繫統的計算模型——有窮自動機，它也是計算機科學中基本的數學模型，第5章介紹早的並發計算模型——Petri網。

中篇（第6和第7章）為形式規約篇，著重討論並發繫統屬性的主要規約方法及應用。第6章介紹真假值依賴時間而變化的非經典邏輯——時序邏輯，它是描述並發繫統屬性的重要工具，第7章重點闡述並發繫統基本的兩類屬性——安全性和活性，及其時序邏輯描述方法。

下篇（第8～12章）為形式驗證篇，著重介紹主要的形式驗證方法及相關驗證工具。第8章介紹基於時序邏輯的演繹證明方法及驗證工具STeP，第9~12章重點闡述模型檢測方法、工具及其在並發、實時及混成繫統中的應用，這是形式化方法自動化的核心內容，也是本書的重點。其中第9章介紹經典的模型檢測算法、驗證工具SPIN及應用，第10章介紹基於二叉判定圖(BDD)的符號模型檢測方法、驗證工具SMV及應用，第11章介紹模型檢測與概率分析方法相結合的概率模型檢測方法、驗證工具PRISM及應用，第12章介紹實時與混成繫統的模型檢測方法、驗證工具UPPAAL及應用。

全書提供了大量應用實例，每章後均附有習題。

本書由張廣泉擔任主編，負責全書內容的組稿、統稿和修改工作。顧玉磊、宋相君、宋振華、項周坤、瀋興勤、鄭林峰、張紅美等參與了書稿整理、文字錄入和校對工作，祝義副教授、孫慶英老師、魏慧老師等參與了部分書稿的校對工作，在此對他們的辛勤勞動表示感謝。此外，在本書的編寫過程中，參考了大量國內外相關文獻，在此對本書所引用文獻的作者深表感謝。

本書編寫工作得到江蘇省“十二五”高等學校重點教材立項建設和蘇州大學教材培育項目的資助，以及江蘇省自然科學基金（BK2011281）、中國科學院軟件研究所計算機科學國家重點實驗室開放課題（SYSKF0908、SYSKF1201）、南京大學計算機軟件新技術國家重點實驗室開放課題（KFKT2012B15）的支持和幫助。中國科學院軟件研究所焦莉研究員副研究員、朱雪陽博士、晏榮傑博士仔細閱讀了本書初稿，提出了許多重要的修改意見與建議，在此表示衷心感謝。本書的編寫還得到中國科學院軟件研究所周巢塵院士、林惠民院士、瀋一棟研究員、張健研究員、張文輝研究員、詹乃軍研究員、南京大學李宣東教授、上海大學繆淮扣教授、南京航空航天大學黃志球教授、東南大學李必信教授等及蘇州大學教務部和計算機科學與技術學院的關心和支持，清華大學出版社黃芝和薛陽編輯為本書出版做了大量工作，在此一並表示誠摯的感謝。

由於編者水平有限，書中難免有不當之處，敬請讀者批評指正。

張廣泉
2015年10月於蘇州大學天賜莊校區