第一章 概述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 我们要去往何方"para" label-module="para">
1. 9 本书的组织结构 18
习题 19
第二章 可信性需求 21
2. 1 为什么需要可信性需求 21
2. 2 可信性概念的演变过程 21
2. 3 术语的作用 23
2. 4 什么是系统"para" label-module="para">
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 为什么要考虑应用系统的可信性"para" label-module="para">
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 软件哪里出错了"para" label-module="para">
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
" 2100433B
