第一章 概述 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 什么是系统？ 24
2.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