形式化方法導(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ù)依賴(lài)系統(tǒng)

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

3.3本章小結(jié)

習(xí)題3

第4章自動(dòng)機(jī)

4.1有窮自動(dòng)機(jī)

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

4.1.2形式定義

4.1.3判定算法

4.2Büchi自動(dòng)機(jī)

4.2.1ω有窮自動(dòng)機(jī)簡(jiǎn)介

4.2.2Büchi自動(dòng)機(jī)

4.2.3應(yīng)用舉例

4.3本章小結(jié)

習(xí)題4

第5章Petri網(wǎng)

5.1庫(kù)所/變遷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線(xiàn)性時(shí)序邏輯

6.1.1LTL語(yǔ)法

6.1.2LTL語(yǔ)義

6.1.3應(yīng)用舉例

6.2分支時(shí)序邏輯

6.2.1CTL語(yǔ)法

6.2.2CTL語(yǔ)義

6.2.3應(yīng)用舉例

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

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自動(dòng)定理證明方法

8.2.1SAT求解算法

8.2.2SMT求解技術(shù)

8.2.3ATP方法小結(jié)

8.3交互式定理證明方法

8.3.1主要證明輔助工具簡(jiǎn)介

8.3.2應(yīng)用舉例

8.3.3ITP方法小結(jié)

8.4本章小結(jié)

習(xí)題8

第9章模型檢測(cè)

9.1基本概念

9.2模型檢測(cè)算法

9.2.1CTL模型檢測(cè)算法

9.2.2LTL模型檢測(cè)算法

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

9.3.1驗(yàn)證工具SPIN

9.3.2應(yīng)用舉例

9.4本章小結(jié)

習(xí)題9

第10章符號(hào)模型檢測(cè)

10.1二叉判定圖

10.1.1基本概念

10.1.2約簡(jiǎn)方法

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

10.2CTL符號(hào)模型檢測(cè)

10.2.1基本方法

10.2.2驗(yàn)證工具SMV

10.2.3應(yīng)用舉例

10.3LTL符號(hào)模型檢測(cè)簡(jiǎn)介

10.4本章小結(jié)

習(xí)題10

第11章概率模型檢測(cè)

11.1概率模型

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

11.1.2馬爾可夫決策過(guò)程

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

11.2概率時(shí)序邏輯

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

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

11.3概率模型檢測(cè)工具及應(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í)間自動(dòng)機(jī)

12.1.1語(yǔ)法

12.1.2語(yǔ)義

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

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

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

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

12.3.1基本方法

12.3.2驗(yàn)證工具UPPAAL

12.3.3應(yīng)用舉例

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

12.4.1混成自動(dòng)機(jī)

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

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

12.5本章小結(jié)

習(xí)題12

參考文獻(xiàn)