形式化方法導(dǎo)論（第2版）

目錄

第1章緒論

1.1形式化方法的發(fā)展歷程

1.2形式化方法的基本內(nèi)容

1.2.1系統(tǒng)建模

1.2.2形式規(guī)約

1.2.3形式驗證

1.3本章小結(jié)

習(xí)題1

第2章程序正確性證明

2.1Floyd前后斷言法

2.1.1基本概念

2.1.2證明方法

2.1.3應(yīng)用舉例

2.2Hoare公理化方法

2.2.1基本概念

2.2.2證明方法

2.2.3應(yīng)用舉例

2.3Dijkstra最弱前置條件方法

2.3.1基本概念

2.3.2證明方法

2.3.3應(yīng)用舉例

2.4本章小結(jié)

習(xí)題2

上篇系 統(tǒng) 建 模

第3章遷移系統(tǒng)

3.1基本概念

3.1.1形式定義

3.1.2遷移圖

3.1.3計算

3.2應(yīng)用舉例

3.2.1時序電路

3.2.2數(shù)據(jù)依賴系統(tǒng)

3.2.3并發(fā)和交錯

3.3本章小結(jié)

習(xí)題3

第4章自動機(jī)

4.1有窮自動機(jī)

4.1.1有窮狀態(tài)系統(tǒng)

4.1.2形式定義

4.1.3判定算法

4.2Büchi自動機(jī)

4.2.1ω有窮自動機(jī)簡介

4.2.2Büchi自動機(jī)

4.2.3應(yīng)用舉例

4.3本章小結(jié)

習(xí)題4

第5章Petri網(wǎng)

5.1庫所/變遷Petri網(wǎng)

5.1.1基本概念

5.1.2基本性質(zhì)

5.1.3分析方法

5.1.4應(yīng)用舉例

5.2謂詞/變遷Petri網(wǎng)

5.2.1基本概念

5.2.2應(yīng)用舉例

5.3著色Petri網(wǎng)

5.3.1基本概念

5.3.2應(yīng)用舉例

5.4本章小結(jié)

習(xí)題5

中篇形 式 規(guī) 約

第6章時序邏輯

6.1線性時序邏輯

6.1.1LTL語法

6.1.2LTL語義

6.1.3應(yīng)用舉例

6.2分支時序邏輯

6.2.1CTL語法

6.2.2CTL語義

6.2.3應(yīng)用舉例

6.3區(qū)間時序邏輯簡介

6.4本章小結(jié)

習(xí)題6

第7章并發(fā)系統(tǒng)屬性

7.1基本概念

7.2安全性

7.2.1形式定義

7.2.2形式描述

7.2.3應(yīng)用舉例

7.3活性

7.3.1形式定義

7.3.2形式描述

7.3.3應(yīng)用舉例

7.4本章小結(jié)

習(xí)題7

下篇形 式 驗 證

第8章定理證明

8.1時序邏輯演繹驗證方法

8.1.1PLTL邏輯系統(tǒng)

8.1.2MannaPnueli演繹規(guī)則方法

8.1.3驗證工具STeP及應(yīng)用

8.2自動定理證明方法

8.2.1SAT求解算法

8.2.2SMT求解技術(shù)

8.2.3ATP方法小結(jié)

8.3交互式定理證明方法

8.3.1主要證明輔助工具簡介

8.3.2應(yīng)用舉例

8.3.3ITP方法小結(jié)

8.4本章小結(jié)

習(xí)題8

第9章模型檢測

9.1基本概念

9.2模型檢測算法

9.2.1CTL模型檢測算法

9.2.2LTL模型檢測算法

9.3模型檢測工具及應(yīng)用

9.3.1驗證工具SPIN

9.3.2應(yīng)用舉例

9.4本章小結(jié)

習(xí)題9

第10章符號模型檢測

10.1二叉判定圖

10.1.1基本概念

10.1.2約簡方法

10.1.3Apply操作及應(yīng)用

10.2CTL符號模型檢測

10.2.1基本方法

10.2.2驗證工具SMV

10.2.3應(yīng)用舉例

10.3LTL符號模型檢測簡介

10.4本章小結(jié)

習(xí)題10

第11章概率模型檢測

11.1概率模型

11.1.1離散時間馬爾可夫鏈

11.1.2馬爾可夫決策過程

11.1.3連續(xù)時間馬爾可夫鏈

11.2概率時序邏輯

11.2.1概率計算樹邏輯

11.2.2連續(xù)隨機(jī)邏輯

11.3概率模型檢測工具及應(yīng)用

11.3.1驗證工具PRISM

11.3.2應(yīng)用舉例

11.4本章小結(jié)

習(xí)題11

第12章實時與混成系統(tǒng)驗證

12.1時間自動機(jī)

12.1.1語法

12.1.2語義

12.2實時邏輯

12.2.1時間計算樹邏輯

12.2.2度量區(qū)間時序邏輯

12.3實時系統(tǒng)模型檢測

12.3.1基本方法

12.3.2驗證工具UPPAAL

12.3.3應(yīng)用舉例

12.4混成系統(tǒng)驗證簡介

12.4.1混成自動機(jī)

12.4.2微分動態(tài)邏輯

12.4.3混成系統(tǒng)模型檢測

12.5本章小結(jié)

習(xí)題12

參考文獻(xiàn)