形式化方法是軟件工程專業的核心課程，但相關教材稀缺，本書彌補了這一空白，內容全面，適合教學。

●第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
參考文獻

形式化方法是指有嚴格數學基礎的軟件和繫統開發方法，支持軟件與繫統的規約、設計、驗證與演化等活動。隨著軟件可信需求的不斷增長，形式化方法的重要性和關注度日益提高。本書共12章，第1章概述形式化方法，第2章介紹形式化方法發展早期的經典內容，其餘部分共分3篇：上篇（第3~5章）為繫統建模篇，著重介紹遷移繫統、有窮自動機、Petri網等基本計算模型；中篇（第6和第7章）為形式規約篇，著重討論時序邏輯及其在並發繫統屬性描述的應用；下篇（第8~12章）為形式驗證篇，著重介紹定理證明方法和並發、實時及混成繫統的各種模型檢測方法及相關驗證工具。全書提供了大量應用實例，每章後均附有習題。本書適合作為高等院校計算機、軟件工程、人工智能、網絡工程、信息安全、自動化等專業高年級本科生、研究生的教材，同時可供相關領域的研究人員和技術開發人員參考。