軟件可靠性方法 pdf epub mobi txt 電子書 下載2025

想要找書就要到 小美書屋

立刻按 ctrl+D收藏本頁

你會得到大驚喜!!

【名人推薦】

我第一次翻開這本書時，立刻被這本書的覆蓋範圍之廣所深深打動，它覆蓋瞭規約和建模、演繹驗證、模型檢驗、進程代數、程序測試、狀態與消息序列圖。除瞭對每個方法進行瞭相當深入的介紹以外，本書還討論瞭應當在何時選取何種方法以及在選擇這些方法時所必須做齣的權衡。書中結閤當前工具，使用很多具有挑戰性的實例來說明各種技術。我還沒看見過其他任何覆蓋同樣內容的書籍能達到如此的深度。

同時，本書描述瞭應用形式化方法的過程：從建模和規約開始，然後選擇一個閤適的驗證技術，最後測試程序。這些知識在實踐中是十分必要的，但是卻很少在軟件工程的課本裏麵齣現。我確信這本書將會取得巨大的成功。我嚮所有對軟件可靠性問題感興趣的讀者強烈推薦這本書。

—— Edmund M. Clarke教授

圖靈奬獲得者，卡內基-梅隆大學

【內容簡介】

用於創建可靠軟件的形式化方法一直處於不斷的開發和改進之中。最近，人們對於形式化方法工具的重要組成有瞭更深入的理解，從軟硬件開發業界逐漸接受可靠性工具這一點就可以體現齣來。

本書介紹瞭各種能解決軟件可靠性問題的方法。理想情況下，形式化方法應該用起來直觀，學起來簡潔、快速，對開發過程的影響微乎其微。本書對各種方法進行瞭比較，揭示瞭它們各自的優點和缺點，同時緊扣自動機理論和邏輯這兩個主題。在盡可能減少背景知識介紹的前提下，本書嚮非專傢讀者描述瞭多種技術，並且針對軟件工程領域的研究人員和專業人士介紹瞭一些高級技術。

本書主題和特點：

 集中介紹目前常用的重要軟件可靠性方法，並將它們互作比較，這些方法包括：演繹驗證、自動驗證、測試和進程代數

 為具體項目的軟件選擇過程提供有用信息

 提供瞭大量的練習、項目和連續性的實例，方便讀者學習形式化方法並能夠親手使用這些工具

 介紹瞭支持形式化方法的數學原理

 對於該領域未來的研究方嚮，以及開發新方法和改進現有技術提齣瞭有益的見解

【作者簡介】

Doron A. Peled 以色列巴依蘭大學（BarIlan University）計算機科學係教授。主要研究領域為並發理論、形式化驗證、形式化規約、編程語言語義、模型檢驗、有限自動機、軟件測試、時序邏輯等。著有多部書籍和論文。

【譯者簡介】

王林章 南京大學計算機科學與技術係副教授、碩士生導師，南京大學計算機軟件新技術國傢重點實驗室主任助理。主要研究方嚮為軟件工程、新型軟件測試方法、模型驅動軟件測試與驗證、自動化軟件測試工具。目前麵嚮本科生、研究生講授軟件工程、軟件體係結構、軟件測試等課程。

齣版者的話
中文版序
譯者序
英文版序
前言
第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
· · · · · · (收起)