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

目錄

第1章緒論

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

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

1.2.1系統(tǒng)建模

1.2.2形式規(guī)約

1.2.3形式驗(yàn)證

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計(jì)算

3.2應(yīng)用舉例

3.2.1時(shí)序電路

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

3.2.3并發(fā)和交錯(cuò)

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章時(shí)序邏輯

6.1線性時(shí)序邏輯

6.1.1LTL語法

6.1.2LTL語義

6.1.3應(yīng)用舉例

6.2分支時(shí)序邏輯

6.2.1CTL語法

6.2.2CTL語義

6.2.3應(yīng)用舉例

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

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

下篇形 式 驗(yàn) 證

第8章定理證明

8.1時(shí)序邏輯演繹驗(yàn)證方法

8.1.1PLTL邏輯系統(tǒng)

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

8.1.3驗(yàn)證工具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驗(yàn)證工具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驗(yàn)證工具SMV

10.2.3應(yīng)用舉例

10.3LTL符號模型檢測簡介

10.4本章小結(jié)

習(xí)題10

第11章概率模型檢測

11.1概率模型

11.1.1離散時(shí)間馬爾可夫鏈

11.1.2馬爾可夫決策過程

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

11.2概率時(shí)序邏輯

11.2.1概率計(jì)算樹邏輯

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

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

11.3.1驗(yàn)證工具PRISM

11.3.2應(yīng)用舉例

11.4本章小結(jié)

習(xí)題11

第12章實(shí)時(shí)與混成系統(tǒng)驗(yàn)證

12.1時(shí)間自動機(jī)

12.1.1語法

12.1.2語義

12.2實(shí)時(shí)邏輯

12.2.1時(shí)間計(jì)算樹邏輯

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

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

12.3.1基本方法

12.3.2驗(yàn)證工具UPPAAL

12.3.3應(yīng)用舉例

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

12.4.1混成自動機(jī)

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

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

12.5本章小結(jié)

習(xí)題12

參考文獻(xiàn)