齣版者的話
中文版序
譯者序
英文版序
前言
第1章　引言1
1.1　形式化方法2
1.2　開發與學習形式化方法3
1.3　使用形式化方法5
1.4　應用形式化方法6
1.5　本書概要7
第2章　預備知識8
2.1　集閤錶示法8
2.2　字符串和語言9
2.3　圖10
2.4　計算復雜度和可計算性12
2.5　擴展閱讀16
第3章　邏輯和定理證明17
3.1　一階邏輯17
3.2　項17
3.2.1　賦值和解釋18
3.2.2　多個論域上的結構19
3.3　一階公式19
3.4　命題邏輯23
3.5　證明一階邏輯公式24
3.5.1　正嚮推理25
3.5.2　反嚮推理26
3.6　證明係統的屬性26
3.6.1　正確性27
3.6.2　完備性27
3.6.3　可判定性27
3.6.4　結構完備性28
3.7　證明命題邏輯屬性28
3.8　一個實用的證明係統29
3.9　證明示例31
3.10　機器輔助證明37
3.11　機械化定理證明器39
3.12　擴展閱讀39
第4章　軟件係統建模40
4.1　順序係統、並發係統及反應式係統41
4.2　狀態42
4.3　狀態空間43
4.4　轉換係統44
4.5　轉換的粒度47
4.6　為程序建模的例子48
4.6.1　整數除法48
4.6.2　計算組閤數49
4.6.3　Eratosthenes篩法50
4.6.4　互斥52
4.7　非確定性轉換53
4.8　將命題變量賦給狀態54
4.9　閤並狀態空間55
4.10　綫性視角56
4.11　分支視角57
4.12　公平性58
4.13　偏序視角61
4.13.1　一個銀行係統的例子61
4.13.2　綫性化和全局狀態63
4.13.3　一個簡單的例子64
4.13.4　偏序模型的應用65
4.14　形式化建模65
4.15　一個項目的建模67
4.16　擴展閱讀68
第5章　形式化規約69
5.1　規約機製的屬性69
5.2　綫性時序邏輯70
5.3　公理化LTL74
5.4　LTL規約示例74
5.4.1　交通燈74
5.4.2　順序程序的屬性75
5.4.3　互斥76
5.4.4　公平性條件76
5.5　無限字上的自動機77
5.6　使用Büchi自動機作為規約79
5.7　確定性Büchi自動機80
5.8　其他規約機製81
5.9　復雜的規約83
5.10　規約的完整性83
5.11　擴展閱讀84
第6章　自動驗證85
6.1　狀態空間搜索86
6.2　狀態錶示方法87
6.3　自動機結構體係88
6.4　閤並Büchi自動機89
6.4.1　廣義Büchi自動機90
6.4.2　將廣義Büchi自動機轉換為簡單Büchi自動機91
6.5　Büchi自動機求補92
6.6　檢驗空集93
6.7　模型檢驗範例94
6.8　將LTL轉換為自動機95
6.9　模型檢驗的復雜度100
6.10　錶示公平性102
6.11　檢驗LTL規約102
6.12　安全屬性103
6.13　狀態空間爆炸問題104
6.14　模型檢驗的優點105
6.15　模型檢驗的缺點105
6.16　選擇自動驗證工具105
6.17　模型檢驗項目105
6.18　模型檢驗工具106
6.19　擴展閱讀106
第7章　演繹式軟件驗證107
7.1　流程圖程序的驗證107
7.2　含數組變量的驗證111
7.2.1　含數組變量賦值的問題112
7.2.2　修改證明係統112
7.3　完全正確性114
7.4　公理式程序驗證117
7.4.1　賦值公理117
7.4.2　空語句公理117
7.4.3　左強化規則117
7.4.4　右弱化規則118
7.4.5　順序組閤規則118
7.4.6　if-then-else規則118
7.4.7　while規則118
7.4.8　begin-end規則119
7.4.9　示例：整數除法119
7.5　並發程序的驗證121
7.6　演繹驗證的優點124
7.7　演繹驗證的缺點125
7.8　證明係統的正確性和完備性126
7.9　組閤性127
7.10　演繹驗證工具128
7.11　擴展閱讀128
第8章　進程代數與等價關係129
8.1　進程代數130
8.2　通信係統的演算131
8.2.1　動作前綴131
8.2.2　選擇132
8.2.3　並發組閤132
8.2.4　限製符133
8.2.5　重標記133
8.2.6　等式定義133
8.2.7　agent 0135
8.2.8　傳值agent135
8.3　示例：Dekker算法135
8.4　建模問題137
8.5　agent之間的等價性138
8.5.1　跡等價139
8.5.2　失敗等價139
8.5.3　模擬等價140
8.5.4　互模擬和弱互模擬等價142
8.6　等價關係的層級142
8.7　用進程代數研究並發143
8.8　計算互模擬等價145
8.9　LOTOS147
8.10　進程代數工具148
8.11　擴展閱讀148
第9章　軟件測試150
9.1　審查和走查151
9.2　控製流覆蓋準則152
9.2.1　語句覆蓋153
9.2.2　邊覆蓋153
9.2.3　條件覆蓋153
9.2.4　邊/條件覆蓋154
9.2.5　條件組閤覆蓋154
9.2.6　路徑覆蓋154
9.2.7　不同覆蓋準則的比較155
9.2.8　循環覆蓋155
9.3　數據流覆蓋準則155
9.4　傳播路徑條件157
9.4.1　示例：GCD程序159
9.4.2　含有輸入語句的路徑160
9.5　等價類劃分160
9.6　待測代碼預處理160
9.7　檢查測試套件161
9.8　組閤性162
9.9　黑盒測試163
9.10　概率測試164
9.11　測試的優點165
9.12　測試的缺點166
9.13　測試工具166
9.14　擴展閱讀166
第10章　組閤形式化方法167
10.1　抽象167
10.2　組閤測試與模型檢驗171
10.2.1　直接檢驗171
10.2.2　黑盒係統172
10.2.3　組閤鎖自動機172
10.2.4　黑盒死鎖檢測172
10.2.5　一緻性測試173
10.2.6　檢驗重置的可靠性175
10.2.7　黑盒檢驗176
10.3　淨室方法177
10.3.1　驗證177
10.3.2　證明審查177
10.3.3　測試177
10.4　擴展閱讀178
第11章　可視化179
11.1　在形式化方法中運用可視化179
11.2　消息序列圖180
11.3　可視化流程圖和狀態機182
11.4　層次狀態圖184
11.4.1　層次化狀態184
11.4.2　統一的齣口和入口185
11.4.3　並發185
11.4.4　輸入和輸齣185
11.5　程序文本的可視化186
11.6　Petri網186
11.7　可視化工具188
11.8　擴展閱讀188
結束語189
參考文獻191
· · · · · · (收起)