形式化方法導論

《形式化方法導論》是2015年12月1日出版的圖書，作者是張廣泉。

內容簡介

《形式化方法導論》是由12章構成，主要論述有嚴格數學基礎的軟體和系統開發方法，支持軟體與系統的規約、設計、驗證與演化等活動的書籍。

形式化方法是指有嚴格數學基礎的軟體和系統開發方法，支持軟體與系統的規約、設計、驗證與演化等活動。隨著軟體可信需求的不斷增長，形式化方法的重要性和關注度日益提高。 全書共12章，第1章概述形式化方法，第2章介紹形式化方法發展早期的經典內容，其餘部分共分3篇： 上篇（第3～5章）為系統建模篇，著重介紹遷移系統、有窮自動機、Petri網等基本計算模型； 中篇（第6和第7章）為形式規約篇，著重討論時序邏輯及其在並發系統屬性描述的套用； 下篇（第8～12章）為形式驗證篇，除介紹演繹證明方法外，著重介紹驗證並發、實時及混成系統的各種模型檢測方法及相關驗證工具。全書提供了大量套用實例，每章後均附有習題。

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

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

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

圖書目錄

第1章緒論

1.1形式化方法的發展歷程

1.2形式化方法的基本內容

1.2.1系統建模

1.2.2形式規約

1.2.3形式驗證

1.3本章小結

習題1

第2章程式正確性證明

2.1前後斷言法

2.1.1基本概念

2.1.2證明方法

2.1.3套用舉例

2.2公理化方法

2.2.1基本概念

2.2.2證明方法

2.2.3套用舉例

2.3最弱前置條件方法

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驗證圖方法

8.1.4套用舉例

8.2驗證工具STeP

8.2.1STeP簡介

8.2.2STeP使用

8.3STeP套用舉例

8.3.1建模

8.3.2驗證

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

參考文獻