《軟體工程師可信計算基礎》是2014年12月國防工業出版社出版的圖書，作者是陸民燕、張虹。
基本介紹
內容簡介,圖書目錄,
內容簡介
本書為美國維吉尼亞大學John Knight 教授的最新著作,是計算機系統可信性領域的前沿著作。書中提出了一套完整的計算機系統可信性概念和術語體系,介紹了可信性需求、可信性分析、可信性評估的基本方法,並重點對錯誤、故障、威脅等相關概念進行了闡述和區分,詳細討論了故障避免、故障消除、容錯和故障預測這四種故障處理措施,並配以大量的案例進行說明和分析。
本書不僅詳細介紹了計算機系統可信性領域的相關概念、技術和方法, 完整得提出了一套計算機系統可信性術語體系,還凝聚了作者多年從事軟體可信性研究工作所獲得的寶貴經驗,對於國內正在興起的可信性研究具有重要的指導意義和參考價值。
圖書目錄
第一章 概述1
1. 1 可信性的元素 1
1. 1. 1 一個警示性的故事 1
1. 1. 2 為什麼要研究可信性 3
1. 2 軟體工程師的角色 4
1. 3 對於計算機的依賴 6
1. 4 一些遺憾的失效 7
1. 4. 1 “阿麗亞娜冶V 火箭 7
1. 4. 2 大韓航空801 航班 8
1. 4. 3 火星氣候軌道飛行器 8
1. 4. 4 火星極地登入器 9
1. 4. 5 其他重要的事故 9
1. 4. 6 如何考慮失效 10
1. 5 失效的後果 10
1. 5. 1 不明顯的失效後果 11
1. 5. 2 失效帶來的意外成本 11
1. 5. 3 後果的種類 12
1. 5. 4 確定失效後果 13
1. 6 對於可信性的需求 13
1. 7 系統和它們的可信性需求 14
1. 7. 1 關鍵系統 14
1. 7. 2 幫助構建系統的系統 16
1. 7. 3 與其他系統互動的系統 17
1. 8 我們要去往何方? 17
1. 9 本書的組織結構 18
習題 19
第二章 可信性需求 21
2. 1 為什麼需要可信性需求 21
2. 2 可信性概念的演變過程 21
2. 3 術語的作用 23
2. 4 什麼是系統? 242. 5 需求和規格說明 26
2. 6 失效 27
2. 6. 1 服務失效的概念 27
2. 6. 2 服務失效的來源 28
2. 6. 3 需求和規格說明的實踐觀點 30
2. 6. 4 服務失效的視角 30
2. 6. 5 告知用戶失效 31
2. 7 可信性及其屬性 32
2. 7. 1 可靠性 34
2. 7. 2 可用性 34
2. 7. 3 每次請求失效 37
2. 7. 4 安全性 37
2. 7. 5 機密性 39
2. 7. 6 完整性 40
2. 7. 7 維修性 41
2. 7. 8 有關保密安全性的辭彙 41
2. 7. 9 信任的概念 41
2. 8 系統、軟體和可信性 42
2. 8. 1 計算機既非不安全也非不保密安全 42
2. 8. 2 為什麼要考慮套用系統的可信性? 43
2. 8. 3 套用系統可信性和計算機 43
2. 9 定義可信性需求 45
2. 9. 1 第一個例子:汽車巡航控制器 46
2. 9. 2 第二個例子:起搏器 47
2. 10 低至合理可行ALARP 49
2. 10. 1 對於ALARP 的需求 49
2. 10. 2 ALARP 概念 50
2. 10. 3 ALARP 胡蘿蔔圖 51
習題 52
第三章 錯誤、故障和危險 56
3. 1 錯誤 56
3. 2 錯誤狀態的複雜性 57
3. 3 故障和可信性 58
3. 3. 1 故障的定義 58
3. 3. 2 識別故障 59
3. 3. 3 故障類型 60
3. 3. 4 實現可信性 60
3. 4 故障的表現 60
3. 5 退化故障 61
3. 5. 1 退化故障機率———浴盆曲線 62
3. 5. 2 退化故障的例子———硬碟 62
3. 6 設計故障 64
3. 7 拜占庭故障 65
3. 7. 1 概念 65
3. 7. 2 拜占庭故障的例子 66
3. 7. 3 拜占庭故障的微妙之處 67
3. 8 組件失效語義 68
3. 8. 3 磁碟驅動器的例子 68
3. 8. 2 實現可預測的失效語義 68
3. 8. 3 軟體失效語義 69
3. 9 可信性的基本原理 69
3. 9. 1 故障避免 70
3. 9. 2 故障排除 71
3. 9. 3 容錯 71
3. 9. 4 故障預測 71
3. 10 預期故障 71
3. 11 危險 72
3. 11. 1 危險的概念 72
3. 11. 2 危險識別 73
3. 11. 3 危險和故障 74
3. 12 構造可信系統 74
習題 76
第四章 可信性分析 78
4. 1 預期故障 78
4. 2 泛化危險的概念 79
4. 3 故障樹分析 79
4. 3. 1 故障樹的基本概念 80
4. 3. 2 基本事件和中間事件 80
4. 3. 3 故障樹的檢查 82
4. 3. 4 故障樹的機率分析 82
4. 3. 5 軟體和故障樹 82
4. 3. 6 故障樹示例 84
4. 3. 7 深度防禦 86
4. 3. 8 故障樹的其他套用 88
4. 4 失效模式、影響和嚴酷度分析 88
4. 4. 1 FMECA 的概念 88
4. 5 危險和可操作性分析 90
4. 5. 1 HazOp 的概念 90
4. 5. 2 基本的HazOp 過程 91
4. 5. 3 HazOp 和計算機系統 91
習題 92
第五章 故障處理 94
5. 1 故障及其處理 94
5. 2 故障避免 95
5. 2. 1 退化故障 95
5. 2. 2 設計故障 95
5. 3 故障消除 96
5. 3. 1 退化故障 96
5. 3. 2 設計故障 96
5. 4 容錯 97
5. 4. 1 熟悉容錯 97
5. 4. 2 定義 97
5. 4. 3 容錯的語義 99
5. 4. 4 容錯的階段 99
5. 4. 5 容錯系統的一個例子 100
5. 5 故障預測 102
5. 5. 1 故障預測過程 102
5. 5. 2 運行環境 102
5. 5. 3 退化故障 103
5. 5. 4 設計故障 103
5. 6 四種故障處理方法的套用 104
5. 7 拜占庭故障處理 105
5. 7. 1 拜占庭將軍 105
5. 7. 2 拜占庭將軍和計算機 106
5. 7. 3 不可能性結果 108
5. 7. 4 拜占庭將軍問題的解決方案 109
習題 110
第六章 退化故障和軟體 112
6. 1 對於軟體的影響 112
6. 2 冗餘 113
6. 2. 1 冗餘和備份 113
6. 2. 2 大規模部件冗餘和小規模部件冗餘 115
6. 2. 3 靜態冗餘和動態冗餘 116
6. 3 冗餘結構 117
6. 3. 1 雙冗餘 118
6. 3. 2 可切換雙冗餘 120
6. 3. 3 N -模組冗餘 125
6. 3. 4 混合冗餘 126
6. 4 量化冗餘的效益 128
6. 4. 1 統計獨立性 128
6. 4. 2 雙冗餘結構 129
6. 5 分散式系統和失效停止計算機 129
6. 5. 1 分散式系統 129
6. 5. 2 計算機的失效語義 130
6. 5. 3 分散式系統的開發 131
6. 5. 4 失效停止概念 131
6. 5. 5 失效停止計算機的實現 132
6. 5. 6 失效停止計算機的軟體編程 133
習題 135
第七章 軟體可信性 137
7. 1 故障和軟體生命周期 137
7. 1. 1 軟體及其脆弱性 138
7. 1. 2 軟體故障處理 139
7. 1. 3 軟體生命周期 139
7. 1. 4 驗證與確認 140
7. 2 形式化技術 141
7. 2. 1 軟體工程中的分析 141
7. 2. 2 形式化需求規格說明 143
7. 2. 3 形式化驗證 144
7. 2. 4 “正確性冶這一術語的使用 144
7. 3 通過模型檢驗進行驗證 144
7. 3. 1 模型檢驗的作用 144
7. 3. 2 分析模型 145
7. 3. 3 使用模型檢測器 146
7. 4 通過構造獲得正確性 147
7. 5 通過構造獲得正確性的方法 147
7. 6 通過構造獲得正確性———綜合 149
7. 6. 1 從形式化需求規格說明生成代碼 149
7. 6. 2 基於模型開發的優點 150
7. 6. 3 基於模型開發的系統實例 151
7. 6. 4 Mathworks Simulink 襅 152
7. 7 通過構造獲得正確性———精化 153
7. 8 軟體故障避免 154
7. 8. 1 嚴格的開發過程 154
7. 8. 2 恰當的符號 156
7. 8. 3 適用所有產品的綜合標準 156
7. 8. 4 支持工具 157
7. 8. 5 受到適當培訓的員工 157
7. 8. 6 形式化技術 157
7. 9 軟體故障消除 158
7. 9. 1靜態分析 158
7. 9. 2 動態分析 159
7. 9. 3 消除故障———根源分析 160
7. 10 管理軟體故障避免和故障消除 161
7. 10. 1 故障免除的屬性 161
7. 11 有關軟體可信性的誤解 163
習題 165
第八章 軟體需求規格說明中的故障避免 167
8. 1 需求規格說明的作用 167
8. 2 自然語言的問題 168
8. 3 需求規格說明的問題 169
8. 3. 1 需求規格說明的缺陷 169
8. 3. 2 需求規格說明的演化 169
8. 4 形式化語言 171
8. 4. 1 形式化句法和語義 171
8. 4. 2 形式化語言的好處 172
8. 4. 3 形式化語言的格式 174
8. 4. 4 形式化語言的類型 175
8. 4. 5 離散數學和形式化需求規格說明 175
8. 4. 6 操作前後的狀態 176
8. 4. 7 一個簡單的需求規格說明 176
8. 5 基於模型的需求規格說明 177
8. 5. 1 使用基於模型的需求規格說明 178
8. 6 聲明性語言Z 179
8. 6. 1 集合 180
8. 6. 2 命題和謂詞 181
8. 6. 3 量詞 182
8. 6. 4 叉積 183
8. 6. 5 關係、序列和函式 183
8. 6. 6 模式 184
8. 6. 7 模式演算 185
8. 7 一個簡單的例子 185
8. 8 一個詳細的例子 187
8. 8. 1 例子版本1 187
8. 8. 2 例子版本2 188
8. 8. 3 簡單例子版本3 190
8. 8. 4 簡單例子版本4 191
8. 9 形式化需求規格說明開發概述 192
習題 193
第九章 軟體實現中的故障避免 196
9. 1 軟體實現 196
9. 1. 1 軟體實現的工具支持 196
9. 1. 2 開發一個軟體實現 197
9. 1. 3 軟體哪裡出錯了? 198
9. 2 程式語言 199
9. 2. 1 C 語言 200
9. 3 Ada 語言概述 201
9. 3. 1 Ada 語言的發明動機 201
9. 3. 2 基本特性 202
9. 3. 3 包 205
9. 3. 4 並發和實時編程 205
9. 3. 5 分離式編譯 205
9. 3. 6 異常 206
9. 4 編程標準 206
9. 4. 1 編程標準和程式語言 206
9. 4. 2 編程標準和故障避免 207
9. 5 通過構造獲得正確性———SPARK 209
9. 5. 1 SPARK 開發的概念 209
9. 5. 2 SPARK Ada 子集 211
9. 5. 3 SPARK 標註 212
9. 5. 4 核心標註 213
9. 5. 5 證明性標註 215
9. 5. 6 循環不變數 217
9. 5. 7 SPARK 工具 220
習題 221
第十章 軟體故障消除 224
10. 1 為什麼要故障消除 224
10. 2 審查 225
10. 2. 1 人工產品和缺陷 226
10. 2. 2 Fagan 審查 227
10. 2. 3 有效的評審 229
10. 2. 4 階段審查 230
10. 3 測試 233
10. 3. 1 窮舉測試 233
10. 3. 2 測試的作用 234
10. 3. 3 測試過程 235
10. 3. 4 軟體形式 235
10. 3. 5 輸出檢查 236
10. 3. 6 測試充分性 237
10. 3. 7 修改條件判斷覆蓋 239
10. 3. 8 測試自動化 240
10. 3. 9 實時系統 241
習題 242
第十一章 軟體容錯 245
11. 1 遭受設計故障的部件 245
11. 2 容錯設計的有關問題 246
11. 2. 1 容錯設計的難點 246
11. 2. 2 自愈系統 248
11. 2. 3 錯誤檢測 248
11. 2. 4 向前和向後錯誤恢復 249
11. 3 軟體複製 250
11. 4 設計多樣性 251
11. 4. 1 N 版本系統 252
11. 4. 2 恢復塊 254
11. 4. 3 交流和對話 255
11. 4. 4 度量設計多樣性 256
11. 4. 5 比較檢查 257
11. 4. 6 一致性比較問題 258
11. 5 數據多樣性 259
11. 5. 1 故障和數據 259
11. 5. 2 數據多樣性的一個特殊案例 260
11. 5. 3 泛化的數據多樣性 261
11. 5. 4 數據再表達 261
11. 5. 5 N -拷貝執行和表決 262
11. 6 定向容錯 263
11. 6. 1 安全核心 264
11. 6. 2 套用隔離 265
11. 6. 3 看門狗定時器 267
11. 6. 4 異常 267
11. 6. 5 執行時間檢查 268
習題 270
第十二章 可信性評價 272
12. 1 評價方法 272
12. 2 定量評價 273
12. 2. 1 基本方法 273
12. 2. 2 壽命試驗 275
12. 2. 3 複合建模 276
12. 2. 4 定量評價的難點 276
12. 3 法定標準 277
12. 3. 1 法定標準的目標 278
12. 3. 2 法定標準例子———RTCA/ DO -178B 279
12. 3. 3 法定標準的優點 283
12. 3. 4 法定標準的缺點 283
12. 4 嚴格的論證 284
12. 4. 1 論證的概念 284
12. 4. 2 安全性舉證 285
12. 4. 3 基於安全性舉證的條例 286
12. 4. 4 構建安全性舉證 287
12. 4. 5 一個簡單的例子 288
12. 4. 6 目標構建符號GSN 291
12. 4. 7 軟體及其論證 292
12. 4. 8 證據類型 294
12. 4. 9 安全性舉證模式 295
12. 5 論證的適用性 296
習題 297
參考文獻 299
索引 307 "
