基本信息
作 者：Doron A.Peled 著 王林章 等 譯
出 版 社：機械工業出版社
ISBN：9787111365532
出版時間：2012-03-01
版 次：1
裝 幀：平裝
開 本：16開
內容簡介
《軟體可靠性方法》通過大量的形式化表示和技術，向讀者提供了各種用於提高軟體可靠性的形式化方法，包括演繹驗證、自動驗證、測試以及進程代數。書中緊緊圍繞邏輯和自動機理論這條主線，比較了各種方法的不同之處，並討論了它們的優缺點。
書中包含一些在多個章節中使用的、具有連續性的實例，有利於讀者通過跟蹤這些實例來了解不同形式化方法的優缺點。本書還包括大量的練習和項目，可以使用軟體可靠性工具來完成。
本書適用於從事軟體開發的廣大讀者，尤其適合作為高年級本科生和碩士生的教材和參考書。
圖書目錄
出版者的話
中文版序
譯者序
英文版序
前言
第1章 引言
1.1 形式化方法
1.2 開發與學習形式化方法
1.3 使用形式化方法
1.4 套用形式化方法
1.5 本書概要
第2章 預備知識
2.1 集合表示法
2.2 字元串和語言
2.3 圖
2.4 計算複雜度和可計算性
2.5 擴展閱讀
第3章 邏輯和定理證明
3.1 一階邏輯
3.2 項
3.2.1 賦值和解釋
3.2.2 多個論域上的結構
3.3 一階公式
3.4 命題邏輯
3.5 證明一階邏輯公式
3.5.1 正向推理
3.5.2 反向推理
3.6 證明系統的屬性
3.6.1 正確性
3.6.2 完備性
3.6.3 可判定性
3.6.4 結構完備性
3.7 證明命題邏輯屬性
3.8 一個實用的證明系統
3.9 證明示例
3.10 機器輔助證明
3.11 機械化定理證明器
3.12 擴展閱讀
第4章 軟體系統建模
4.1 順序系統、並發系統及反應式系統
4.2 狀態
4.3 狀態空間
4.4 轉換系統
4.5 轉換的粒度
4.6 為程式建模的例子
4.6.1 整數除法
4.6.2 計算組合數
4.6.3 Eratosthenes篩法
4.6.4 互斥
4.7 非確定性轉換
4.8 將命題變數賦給狀態
4.9 合併狀態空間
4.10 線性視角
4.11 分支視角
4.12 公平性
4.13 偏序視角
4.13.1 一個銀行系統的例子
4.13.2 線性化和全局狀態
4.13.3 一個簡單的例子
4.13.4 偏序模型的套用
4.14 形式化建模
4.15 一個項目的建模
4.16 擴展閱讀
第5章 形式化規約
5.1 規約機制的屬性
5.2 線性時序邏輯
5.3 公理化LTL
5.4 LTL規約示例
5.4.1 交通燈
5.4.2 順序程式的屬性
5.4.3 互斥
5.4.4 公平性條件
5.5 無限字上的自動機
5.6 使用Büchi自動機作為規約
5.7 確定性Büchi自動機
5.8 其他規約機制
5.9 複雜的規約
5.10 規約的完整性
5.11 擴展閱讀
第6章 自動驗證
6.1 狀態空間搜尋
6.2 狀態表示方法
6.3 自動機結構體系
6.4 合併Büchi自動機
6.4.1 廣義Büchi自動機
6.4.2 將廣義Büchi自動機轉換為簡單Büchi自動機
6.5 Büchi自動機求補
6.6 檢驗空集
6.7 模型檢驗範例
6.8 將LTL轉換為自動機
6.9 模型檢驗的複雜度
6.10 表示公平性
6.11 檢驗LTL規約
6.12 安全屬性
6.13 狀態空間爆炸問題
6.14 模型檢驗的優點
6.15 模型檢驗的缺點
6.16 選擇自動驗證工具
6.17 模型檢驗項目
6.18 模型檢驗工具
6.19 擴展閱讀
第7章 演繹式軟體驗證
7.1 流程圖程式的驗證
7.2 含數組變數的驗證
7.2.1 含數組變數賦值的問題
7.2.2 修改證明系統
7.3 完全正確性
7.4 公理式程式驗證
7.4.1 賦值公理
7.4.2 空語句公理
7.4.3 左強化規則
7.4.4 右弱化規則
7.4.5 順序組合規則
7.4.6 if-then-else規則
7.4.7 while規則
7.4.8 begin-end規則
7.4.9 示例：整數除法
7.5 並發程式的驗證
7.6 演繹驗證的優點
7.7 演繹驗證的缺點
7.8 證明系統的正確性和完備性
7.9 組合性
7.10 演繹驗證工具
7.11 擴展閱讀
第8章 進程代數與等價關係
8.1 進程代數
8.2 通信系統的演算
8.2.1 動作前綴
8.2.2 選擇
8.2.3 並發組合
8.2.4 限制符
8.2.5 重標記
8.2.6 等式定義
8.2.7 agent
8.2.8 傳值agent
8.3 示例：Dekker算法
8.4 建模問題
8.5 agent之間的等價性
8.5.1 跡等價
8.5.2 失敗等價
8.5.3 模擬等價
8.5.4 互模擬和弱互模擬等價
8.6 等價關係的層級
8.7 用進程代數研究並發
8.8 計算互模擬等價
8.9 LOTOS
8.10 進程代數工具
8.11 擴展閱讀
第9章 軟體測試
9.1 審查和走查
9.2 控制流覆蓋準則
9.2.1 語句覆蓋
9.2.2 邊覆蓋
9.2.3 條件覆蓋
9.2.4 邊/條件覆蓋
9.2.5 條件組合覆蓋
9.2.6 路徑覆蓋
9.2.7 不同覆蓋準則的比較
9.2.8 循環覆蓋
9.3 數據流覆蓋準則
9.4 傳播路徑條件
9.4.1 示例：GCD程式
9.4.2 含有輸入語句的路徑
9.5 等價類劃分
9.6 待測代碼預處理
9.7 檢查測試套件
9.8 組合性
9.9 黑盒測試
9.10 機率測試
9.11 測試的優點
9.12 測試的缺點
9.13 測試工具
9.14 擴展閱讀
第10章 組合形式化方法
10.1 抽象
10.2 組合測試與模型檢驗
10.2.1 直接檢驗
10.2.2 黑盒系統
10.2.3 組合鎖自動機
10.2.4 黑盒死鎖檢測
10.2.5 一致性測試
10.2.6 檢驗重置的可靠性
10.2.7 黑盒檢驗
10.3 淨室方法
10.3.1 驗證
10.3.2 證明審查
10.3.3 測試
10.4 擴展閱讀
第11章 可視化
11.1 在形式化方法中運用可視化
11.2 訊息序列圖
11.3 可視化流程圖和狀態機
11.4 層次狀態圖
11.4.1 層次化狀態
11.4.2 統一的出口和入口
11.4.3 並發
11.4.4 輸入和輸出
11.5 程式文本的可視化
11.6 Petri網
11.7 可視化工具
11.8 擴展閱讀
結束語
