第一章 概述

1.1 可信性的元素

1.1.1 一个警示性的故事

1.1.2 为什么要研究可信性

1.2 软件工程师的角色

1.3 对于计算机的依赖

1.4 一些遗憾的失效

1.4.1 “阿丽亚娜”V火箭

1.4.2 大韩航空801航班

1.4.3 火星气候轨道飞行器

1.4.4 火星极地登陆器

1.4.5 其他重要的事故

1.4.6 如何考虑失效

1.5 失效的后果

1.5.1 不明显的失效后果

1.5.2 失效带来的意外成本

1.5.3 后果的种类

1.5.4 确定失效后果

1.6 对于可信性的需求

1.7 系统和它们的可信性需求

1.7.1 关键系统

1.7.2 帮助构建系统的系统

1.7.3 与其他系统交互的系统

1.8 我们要去往何方？

1.9 本书的组织结构

习题

第二章 可信性需求

2.1 为什么需要可信性需求

2.2 可信性概念的演变过程

2.3 术语的作用

2.4 什么是系统？

2.5 需求和规格说明

2.6 失效

2.6.1 服务失效的概念

2.6.2 服务失效的来源

2.6.3 需求和规格说明的实践观点

2.6.4 服务失效的视角

2.6.5 告知用户失效

2.7 可信性及其属性

2.7.1 可靠性

2.7.2 可用性

2.7.3 每次请求失效

2.7.4 安全性

2.7.5 机密性

2.7.6 完整性

2.7.7 维修性

2.7.8 有关保密安全性的词汇

2.7.9 信任的概念

2.8 系统、软件和可信性

2.8.1 计算机既非不安全也非不保密安全

2.8.2 为什么要考虑应用系统的可信性？

2.8.3 应用系统可信性和计算机

2.9 定义可信性需求

2.9.1 第一个例子：汽车巡航控制器

2.9.2 第二个例子：起搏器

2.10 低至合理可行ALARP

2.10.1 对于ALARP的需求

2.10.2 ALARP概念

2.10.3 ALARP胡萝卜图

习题

第三章 错误、故障和危险

3.1 错误

3.2 错误状态的复杂性

3.3 故障和可信性

3.3.1 故障的定义

3.3.2 识别故障

3.3.3 故障类型

3.3.4 实现可信性

3.4 故障的表现

3.5 退化故障

3.5.1 退化故障概率——浴盆曲线

3.5.2 退化故障的例子——硬盘

3.6 设计故障

3.7 拜占庭故障

3.7.1 概念

3.7.2 拜占庭故障的例子

3.7.3 拜占庭故障的微妙之处

3.8 组件失效语义

3.8.3 磁盘驱动器的例子

3.8.2 实现可预测的失效语义

3.8.3 软件失效语义

3.9 可信性的基本原理

3.9.1 故障避免

3.9.2 故障排除

3.9.3 容错

3.9.4 故障预测

3.10 预期故障

3.11 危险

3.11.1 危险的概念

3.11.2 危险识别

3.11.3 危险和故障

3.12 构造可信系统

习题

第四章 可信性分析

4.1 预期故障

4.2 泛化危险的概念

4.3 故障树分析

4.3.1 故障树的基本概念

4.3.2 基本事件和中间事件

4.3.3 故障树的检查

4.3.4 故障树的概率分析

4.3.5 软件和故障树

4.3.6 故障树示例

4.3.7 深度防御

4.3.8 故障树的其他应用

4.4 失效模式、影响和严酷度分析

4.4.1 FMECA的概念

4.5 危险和可操作性分析

4.5.1 HazOp的概念

4.5.2 基本的HazOp过程

4.5.3 HazOp和计算机系统

习题

第五章 故障处理

5.1 故障及其处理

5.2 故障避免

5.2.1 退化故障

5.2.2 设计故障

5.3 故障消除

5.3.1 退化故障

5.3.2 设计故障

5.4 容错

5.4.1 熟悉容错

5.4.2 定义

5.4.3 容错的语义

5.4.4 容错的阶段

5.4.5 容错系统的一个例子

5.5 故障预测

5.5.1 故障预测过程

5.5.2 运行环境

5.5.3 退化故障

5.5.4 设计故障

5.6 四种故障处理方法的应用

5.7 拜占庭故障处理

5.7.1 拜占庭将军

5.7.2 拜占庭将军和计算机

5.7.3 不可能性结果

5.7.4 拜占庭将军问题的解决方案

习题

第六章 退化故障和软件

6.1 对于软件的影响

6.2 冗余

6.2.1 冗余和备份

6.2.2 大规模部件冗余和小规模部件冗余

6.2.3 静态冗余和动态冗余

6.3 冗余结构

6.3.1 双冗余

6.3.2 可切换双冗余

6.3.3 N-模块冗余

6.3.4 混合冗余

6.4 量化冗余的效益

6.4.1 统计独立性

6.4.2 双冗余结构

6.5 分布式系统和失效停止计算机

6.5.1 分布式系统

6.5.2 计算机的失效语义

6.5.3 分布式系统的开发

6.5.4 失效停止概念

6.5.5 失效停止计算机的实现

6.5.6 失效停止计算机的软件编程

习题

第七章 软件可信性

7.1 故障和软件生命周期

7.1.1 软件及其脆弱性

7.1.2 软件故障处理

7.1.3 软件生命周期

7.1.4 验证与确认

7.2 形式化技术

7.2.1 软件工程中的分析

7.2.2 形式化需求规格说明

7.2.3 形式化验证

7.2.4 “正确性”这一术语的使用

7.3 通过模型检验进行验证

7.3.1 模型检验的作用

7.3.2 分析模型

7.3.3 使用模型检测器

7.4 通过构造获得正确性

7.5 通过构造获得正确性的方法

7.6 通过构造获得正确性——综合

7.6.1 从形式化需求规格说明生成代码

7.6.2 基于模型开发的优点

7.6.3 基于模型开发的系统实例

7.6.4 Mathworks Simulink？

7.7 通过构造获得正确性——精化

7.8 软件故障避免

7.8.1 严格的开发过程

7.8.2 恰当的符号

7.8.3 适用所有产品的综合标准

7.8.4 支持工具

7.8.5 受到适当培训的员工

7.8.6 形式化技术

7.9 软件故障消除

7.9.1 静态分析

7.9.2 动态分析

7.9.3 消除故障——根源分析

7.10 管理软件故障避免和故障消除

7.10.1 故障免除的属性

7.11 有关软件可信性的误解

习题

第八章 软件需求规格说明中的故障避免

8.1 需求规格说明的作用

8.2 自然语言的问题

8.3 需求规格说明的问题

8.3.1 需求规格说明的缺陷

8.3.2 需求规格说明的演化

8.4 形式化语言

8.4.1 形式化句法和语义

8.4.2 形式化语言的好处

8.4.3 形式化语言的格式

8.4.4 形式化语言的类型

8.4.5 离散数学和形式化需求规格说明

8.4.6 操作前后的状态

8.4.7 一个简单的需求规格说明

8.5 基于模型的需求规格说明

8.5.1 使用基于模型的需求规格说明

8.6 声明性语言Z

8.6.1 集合

8.6.2 命题和谓词

8.6.3 量词

8.6.4 叉积

8.6.5 关系、序列和函数

8.6.6 模式

8.6.7 模式演算

8.7 一个简单的例子

8.8 一个详细的例子

8.8.1 例子版本1

8.8.2 例子版本2

8.8.3 简单例子版本3

8.8.4 简单例子版本4

8.9 形式化需求规格说明开发概述

习题

第九章 软件实现中的故障避免

9.1 软件实现

9.1.1 软件实现的工具支持

9.1.2 开发一个软件实现

9.1.3 软件哪里出错了？

9.2 编程语言

9.2.1 C语言

9.3 Ada语言概述

9.3.1 Ada语言的发明动机

9.3.2 基本特性

9.3.3 包

9.3.4 并发和实时编程

9.3.5 分离式编译

9.3.6 异常

9.4 编程标准

9.4.1 编程标准和编程语言

9.4.2 编程标准和故障避免

9.5 通过构造获得正确性——SPARK

9.5.1 SPARK开发的概念

9.5.2 SPARK Ada子集

9.5.3 SPARK标注

9.5.4 核心标注

9.5.5 证明性标注

9.5.6 循环不变量

9.5.7 SPARK工具

习题

第十章 软件故障消除

10.1 为什么要故障消除

10.2 审查

10.2.1 人工产品和缺陷

10.2.2 Fagan审查

10.2.3 有效的评审

10.2.4 阶段审查

10.3 测试

10.3.1 穷举测试

10.3.2 测试的作用

10.3.3 测试过程

10.3.4 软件形式

10.3.5 输出检查

10.3.6 测试充分性

10.3.7 修改条件判断覆盖

10.3.8 测试自动化

10.3.9 实时系统

习题

第十一章 软件容错

11.1 遭受设计故障的部件

11.2 容错设计的有关问题

11.2.1 容错设计的难点

11.2.2 自愈系统

11.2.3 错误检测

11.2.4 向前和向后错误恢复

11.3 软件复制

11.4 设计多样性

11.4.1 N版本系统

11.4.2 恢复块

11.4.3 交流和对话

11.4.4 度量设计多样性

11.4.5 比较检查

11.4.6 一致性比较问题

11.5 数据多样性

11.5.1 故障和数据

11.5.2 数据多样性的一个特殊案例

11.5.3 泛化的数据多样性

11.5.4 数据再表达

11.5.5 N-拷贝执行和表决

11.6 定向容错

11.6.1 安全内核

11.6.2 应用隔离

11.6.3 看门狗定时器

11.6.4 异常

11.6.5 执行时间检查

习题

第十二章 可信性评价

12.1 评价方法

12.2 定量评价

12.2.1 基本方法

12.2.2 寿命试验

12.2.3 复合建模

12.2.4 定量评价的难点

12.3 法定标准

12.3.1 法定标准的目标

12.3.2 法定标准例子——RTCA/DO-178B

12.3.3 法定标准的优点

12.3.4 法定标准的缺点

12.4 严格的论证

12.4.1 论证的概念

12.4.2 安全性举证

12.4.3 基于安全性举证的条例

12.4.4 构建安全性举证

12.4.5 一个简单的例子

12.4.6 目标构建符号GSN

12.4.7 软件及其论证

12.4.8 证据类型

12.4.9 安全性举证模式

12.5 论证的适用性

习题

参考文献

索引