形式化方法導論（第2版）

內容簡介

形式化方法是指有嚴格數學基礎的軟體和系統開發方法，支持軟體與系統的規約、設計、驗證與演化等活動。隨著軟體可信需求的不斷增長，形式化方法的重要性和關注度日益提高。

本書共12章，第1章概述形式化方法，第2章介紹形式化方法發展早期的經典內容，其餘部分共分3篇：上篇（第3～5章）為系統建模篇，著重介紹遷移系統、有窮自動機、Petri網等基本計算模型；中篇（第6和第7章）為形式規約篇，著重討論時序邏輯及其在並發系統屬性描述的套用；下篇（第8～12章）為形式驗證篇，著重介紹定理證明方法和並發、實時及混成系統的各種模型檢測方法及相關驗證工具。全書提供了大量套用實例，每章後均附有習題。

本書適合作為高等院校計算機、軟體工程、人工智慧、網路工程、信息安全、自動化等專業高年級本科生、研究生的教材，同時可供相關領域的研究人員和技術開發人員參考。

圖書目錄

第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網

形式化方法導論（第2版）

基本介紹

內容簡介

圖書目錄

相關詞條

熱門詞條