本书专为从事安全关键型嵌入式软件开发的工程师与研究人员撰写，聚焦IEC 61508、ISO 26262等国际标准的实践应用。全书分为背景、项目、设计模式、设计验证、编码、验证六部分，系统阐述了安全关键软件的设计原理、验证方法、工具选型及工程案例，尤其关注软件在硬件故障中的风险控制与灾难规避作用。每章都呈现模块化知识体系，分层展开论述，章末附精选参考文献，兼顾学术深度与工程实用性。本书具有大量跨领域案例，覆盖汽车、医疗、铁路等嵌入式场景。本书源自QNX软件系统培训资料，既适合作为安全关键软件研发指南，也为标准落地提供可操作路径。

本书巧妙结合了嵌入式通用开发与安全关键领域。它不仅系统梳理了各大安全标准的合规实践，更难得的是将方法论融入从设计到验证的全流程，并用可实操的开源工具降低学习门槛。无论是寻求标准解读，还是构建可审计的开发体系，这本书都能为开发团队提供扎实、可信的路线图，是转向高可靠性嵌入式系统开发的必备导航。

译　者　序
3年前，当我们第一次翻开本书英文版时，旋即被作者（原QNX的架构工程师）渊博的知识、丰富的工程经历以及有趣的表达深深地折服。然而随着阅读的深入，我们发现由于本书所呈现的内容之广袤和深刻，若非对软件开发的渊源、与相关学科的联系、软件经典著作乃至英语典故和俗语均有所了解，难以较为全面地理解和掌握本书英文版的精髓。因此，我们有了将其翻译为中文的想法，使之符合中文的表达习惯，并加以背景知识的注释，让以中文为母语的读者能用比阅读英文版少得多的时间全面、准确地获取本书呈现的系统性的知识。环顾四周，虽然与软件开发相关的中文书籍已经汗牛充栋，但在安全关键软件领域，依然难以找到一本如本书般既全面又易懂的著作，本书中文版的出版将补上这一块拼图。
本书从哥德尔的不完备性分析出发，对安全关键软件开发的特点、背景、标准、方法、实例、工具、模型、分析、测试、原理等方面逐一展开介绍。
本书的3名译者均有多年的安全关键嵌入式系统一线开发或流程管理经验。其中，潘怡融负责软件开发部分的翻译；许孟华负责项目及流程管理部分的翻译；李晓华负责书中前言及背景部分的翻译，并对全书进行统稿。另外，本书得以出版并呈现在大家面前，离不开机械工业出版社的各位编辑、审校、排版老师幕后的付出，借此对他们的工作表示衷心的
感谢。
由于译者水平有限，书中难免有错漏、不足之处，敬请广大读者多多包涵，并欢迎大家指正。

前　　言
本书是为从事系统设计、实施和验证工作的人员编写的。在开发通用型嵌入式软件方面他们拥有丰富的经验，但他们现在面对的挑战，是为安全关键型应用提供一个基于软件的系统。具体说来，本书的目标读者往往正在参与创造某个产品，而这个产品必须满足一个或多个牵涉安全关键型应用的国际标准IEC 61508、ISO 26262、EN 50128、EN 50657、IEC 62304 或相关的标准。
软件与安全
媒体似乎总是津津乐道于放疗设备给病人施加了错误剂量的照射、空难或险情，由于FORTRAN代码中遗漏一个逗号而不得不把火箭销毁，以及其他许多诸如此类因软件而起的灾难。而很少会被提及的是，软件是如何在硬件失灵的情况下避免了一场灾难的发生。其中，一个例子是在2009年1月，一架空客公司的飞机在引擎发生硬件故障后成功降落在美国纽约的哈德逊河上。几乎可以肯定，如果没有持续可用的飞行控制软件，这次意外会造成重大人员伤亡。因此，在安全问题上，与硬件相比，软件未必不是力挽狂澜的主角。
我希望这本书能为从事软件设计、实施和验证工作的读者提供一些想法，协助他们实现用软件拯救世界的梦想。
参考文献
要对本书中述及的所有技术进行进一步探索，可供参考的学术文章数以百计。为了给读者提供一种开始这类探索的方法，我在章末提供了参考资料。除了一些心血来潮的例外（例如，1834年Lardner关于多样性编程的论文和1837年Babbage的关于计算引擎的论文），我只收录了我认为能对一个正从事软件开发工作的人起到作用的参考资料。
我对某一话题的想法有时会被参考文献或书目改变，这一般会促使我立即着手开始编写程序，以验证这些概念是否与实际相符。
我是反对向期刊付费去访问已发表的论文的，我相信在章末的参考文献中提到的所有文章都可以从互联网上免费（以及合法）地下载。在一些情况下，例如，在第8章中提到的Kalman 于1960年发表的论文原文，人们可以选择向原始发表期刊支付25美元来获得，也可以通过访问相关教育机构（在本例中，美国北卡罗来纳大学）的网站来免费下载该论文。对此，我把选择权留给读者。
书中经常提到各种国际标准。鉴于这些标准还在持续修订中，我在本书中引用的标准指的是以下版本：
EN 50126 2017/2018 版
EN 50128 2011版
EN 50129 2018版
EN 50657第1版，2017
IEEE 754 2008版
IEEE 24765 2017版
ISO 14971第2版，2007（含2009更新）
ISO/PAS 21448第1版，2019
ISO 26262第2版，2018
ISO 29119第1版，20132016
IEC 61508第2版，2010及IEC TS 61508-3-1:2016
IEC 62304第1版，2006
工具
在示例中我使用了C语言，因为这是与嵌入式编程关联最紧密的语言。掌握一些C语言的知识会对阅读本书有帮助，不过示例都很短，熟悉其他语言的软件工程师读起来应该也不会有什么障碍。
我偶尔也会提到某种特殊的工具。一般来说，我会尽量用开源工具来举例。这倒不是因为它们总是优于同类的商业工具，而是因为这样不会有失公允，除非我是在对所有能够获得的产品都进行仔细比较之后，才选择了这个商业供应商而非另一个。
工具的选择很大程度上还取决于个人的喜好。我们都知道，关于vi和emacs哪个是更好的编辑器的讨论可以上升为一场战争。我才不愿让自己受到这些讨论的影响，在我的感性认知里，vi就是比emacs好得多。
所以，我对工具的选择可能并不一定符合你的偏好。希望每当我提到工具时，能为你寻找合适的供应商提供足够的信息。
第2版更新
本书的第1版于2015年出版，自那以来，安全关键嵌入式软件的领域发生了重大的变化：
在将消除论证应用于安全案例制作后，我发现这是一种极其强大的技术。因此，我在本书的附录A增加了一节来描述这种技术。
预期功能安全（Safety of the Intended Functionality，SOTIF）已成为一个重要的话题，特别是在汽车行业的自治领域。在撰写本书时，这一领域仍然有很大的不确定性，但我仍借此机会提供了一些与其有关的信息；见3.7.2小节。
信息安全（security）对于功能安全（safety）的重要性不断增加：尽管我们早已知道，一个安保不足的系统不可能是一个安全的系统，但随着对安保不足的系统的攻击手段变得日趋老练，将信息安全的内容纳入功能安全的论据变得越来越有必要。这非常不容易，因为功能安全的论据往往变化得很慢，而信息安全的论据却可以在一夜之间发生变化。比如，漏洞（如硬件设备中的Meltdown或Spectre）的发布可以使现有的信息安全论据立刻变得无效；相关内容见5.4节。
新的安全标准（如EN 50657）已经发布，而已有的标准（如ISO 26262）则发生了版本升级。我将本书中引用的ISO 26262更新为该标准的第2版。
我在附录C中增加了一个非常简单的编码处理示例。
读者指出第1版中有各种印刷错误。这些已在第2版中被修正了，但毫无疑问还会出现新的错误。
我们生活在一个有趣的时代一个我们需要应对如风暴般的信息安全问题、由意外系统引发的问题以及由机器学习引发的问题的时代。
致谢
本书改编自QNX软件系统（QNX Software Systems，QSS）公司的一份培训资料，该资料涵盖了用于在部署于汽车、医疗设备、铁路系统、工业自动化系统等领域的安全设备中构建嵌入式软件系统的工具与技术。
这本书中的素材源自我的工作，当然，我并不是一个人在工作。我感谢QNX软件系统公司的管理层，特别是我的直属经理 Jeff Baker和Adam Mallory，他们给了足够的空间让我天马行空，并允许我将培训资料作为本书的基础。
我需要感谢许多人，他们为我提供了想法和挑战。尤其是（按姓氏字母顺序排列）：Dave Banham、John Bell、John Hudepohl、Patrick Lee、Martin Lloyd、Ernst Munter、Rob Paterson、Will Snipes以及Yi Zheng这些多年来与我共事的、充满活力的团队成员。
即便有了想法，撰写一本书也不是简单的任务。我要感谢我的妻子Alison，她握着铅笔一字一句地读完了本书。我已经数不清她用秃了多少支铅笔才把这本书变成了她可以接受的模样。我感谢她，也要感谢Chuck Clark、Adam Mallory和出版商提供的匿名读者，感谢他们极其彻底和详细的校对。
封面图片由Chuck Clark提供。非常感谢他允许我使用这张图片。
关于作者
在某种程度上，今天的我是由三个事件塑造而成的。其中第一个事件我可以准确地说出时间：1968年12月24日晚上8点左右。当时我是一名本科一年级的学生，正在学习通用纯数学的课程。在结束了第一学期的学习后，我从学校回到家中。在离开学校，开始假期之前，我多少有点儿随意地从数学公共休息室的图书馆的书架上抓了一本书。在圣诞夜，我打开了它，第一次看到了库尔特·哥德尔的不完备性分析结果。在那个年代，高中阶段是不教这些元数学分析的。哥德尔的论述对我的思想产生了巨大的冲击。当假期结束后，我回到学校打算进一步学习这种类型的数学时，又难以置信地获得了伦敦经济学院（London School of Economics）的Imre Lakatos的辅导。即使到了现在，在对哥德尔发表论文的背景有了更深刻的了解之后，我仍然认为这些结论是20世纪智力和创造力的顶峰。
最近的一件事件说起来就比较优雅了。2002年时，我突然心血来潮决定要学习弗兰兹·舒伯特的《冬之旅》（Winterreise）套曲中的24首乐曲。十七年后，作为我妻子的伴奏，我仍然在做这件事。有时我会觉得自己揭开了一个盖子，从而得以窥见里面浓烈的情感和深邃的才智。
位于中间的事件与本书的关联则更直接，我在逸事1中对其进行了叙述。这一事件让我开始了对安全关键系统软件开发的研究。
将哥德尔的成果、安全关键软件和《冬之旅》串在一起似乎很奇怪，但我觉得可以把它们中的每一个都视为各自领域顶级的智力挑战。
最近我遇到的一位项目经理曾说，为安全关键应用开发软件和为其他任何应用开发软件并没有什么不同，只不过需要增加大量的文书工作，或许我应该把这本书献给他。

克里斯·霍布斯　　
渥太华　　

克里斯·霍布斯
（Chris Hobbs）　
一位复杂软件系统方面的专家。他曾任职于QNX公司，拥有40年左右的软件开发经验。现为QNX公司顾问，并担任滑铁卢大学客座研究员，继续从事相关领域的研究。他专精于"足够可靠的软件"方向以最低投入和风险开发出满足可靠性要求的软件，尤其擅长开发必须符合IEC 61508、ISO 26262、EN 50128及IEC 62304等国际安全标准要求的安全关键系统软件。他曾是两个安全工作小组的核心成员，致力于为保证案例及复杂系统的安全分析制定指导性文件，并担任这两份文件的主编。

目　　录
译者序
前言
第一部分　背景
第1章　概述　　2
1.1　安全文化　　2
1.2　我们的表达方式　　4
1.2.1　背景材料　　4
1.2.2　为安全关键应用开发产品　　4
1.2.3　标准中推荐的技术　　4
1.2.4　开发工具　　4
1.3　挑选技术的准则　　5
1.4　开发方法　　5
1.5　当今的挑战　　6
1.5.1　信息安全　　6
1.5.2　平衡架构需求的工具　　7
1.5.3　硬件错误检测　　7
1.5.4　时限预测　　7
1.5.5　数据　　7
1.5.6　机器学习　　8
参考文献　　8
第2章　与安全相关的术语　　9
2.1　一般安全术语　　9
2.1.1　危害、风险、缓解和残余
风险　　9
2.1.2　可用性、可靠性和可信度　　10
2.1.3　功能安全　　11
2.1.4　故障、错误和失效　　11
2.1.5　形式化语言、半形式化语言
和非形式化语言　　12
2.1.6　安全、活性和公平　　13
2.1.7　向后及向前错误恢复　　13
2.1.8　意外系统　　13
2.2　软件专用术语　　14
2.2.1　软件　　14
2.2.2　海森堡bug和玻尔bug　　15
2.2.3　实时　　16
2.2.4　契约式编程　　17
参考文献　　17
第3章　安全标准及认证　　18
3.1　标准机构　　18
3.2　认可和认证　　19
3.3　为什么我们需要这些标准　　20
3.4　基于目标的标准和基于规范的
标准　　21
3.5　功能安全标准　　22
3.5.1　IEC 61508　　22
3.5.2　ISO 26262　　25
3.6　IEC 62304和ISO 14971　　28
3.7　机器学习和 SOTIF　　29
3.7.1　机器学习　　29
3.7.2　SOTIF　　30
3.8　流程与标准　　32
3.9　总结　　32
参考文献　　33
第4章　代表性公司　　34
4.1　Alpha设备公司　　34
4.2　Beta零部件公司　　34
4.3　使用经过认证的组件　　35
第二部分　项目
第5章　基础分析　　38
5.1　分析　　38
5.2　相互关系　　39
5.3　危害和风险分析　　39
5.3.1　识别危害和风险　　39
5.3.2　缓解风险　　41
5.3.3　评估残余风险　　42
5.4　安全案例　　43
5.4.1　什么是安全案例　　43
5.4.2　我们为谁创建安全案例　　43
5.4.3　安全案例问题　　43
5.4.4　安全案例内容　　44
5.4.5　安全案例中的信息安全　　46
5.4.6　回溯性安全案例　　47
5.5　失效分析　　47
5.5.1　自下而上的方法　　47
5.5.2　自上而下的方法　　49
5.5.3　以事件为中心的方法　　50
5.6　示例公司会进行的分析　　51
5.6.1　安全手册　　51
5.6.2　危害和风险　　52
5.6.3　安全需求　　52
5.6.4　失效分析　　52
5.6.5　残余风险　　52
5.6.6　安全案例　　53
5.7　总结　　53
参考文献　　53
第6章　认证和未认证的组件　　55
6.1　SOUP的其他名字　　55
6.2　认证或未认证的SOUP　　55
6.3　使用未认证的组件　　56
6.3.1　路线1S　　56
6.3.2　路线2S　　56
6.3.3　路线3S　　57
6.4　使用认证的组件　　59
6.5　对齐发布周期　　60
6.6　示例公司　　60
第三部分　设计模式
第7章　架构平衡　　62
7.1　可用性/可靠性的平衡　　62
7.2　实用性/安全性的平衡　　63
7.3　信息安全/性能/功能安全的
平衡　　64
7.4　性能/可靠性的平衡　　66
7.5　实现手法的平衡　　66
7.6　总结　　66
参考文献　　67
第8章　错误检测和处理　　68
8.1　为何要进行错误检测　　68
8.2　错误检测及其标准　　68
8.3　异常检测　　68
8.3.1　异常检测及其标准　　70
8.3.2　异常检测算法　　70
8.3.3　示例　　71
8.3.4　马尔可夫链　　71
8.3.5　卡尔曼滤波器　　74
8.4　复位　　78
8.4.1　何时进行复位　　79
8.4.2　复位做了什么　　79
8.4.3　选择r4　　80
8.4.4　冗余系统中的复位　　80
8.4.5　复位及其标准　　80
8.5　恢复块　　81
8.6　对多样化监控的一条注解　　82
8.7　总结　　82
参考文献　　83
第9章　预测意外　　84
9.1　设计安全状态　　84
9.1.1　设计安全状态的定义　　84
9.1.2　设计安全状态及其标准　　85
9.1.3　设计安全状态与危险失效　　86
9.2　恢复　　86
9.2.1　恢复技术　　86
9.2.2　你希望恢复吗　　86
9.3　仅崩溃模式　　87
9.4　示例公司对意外事件的预期　　87
9.5　总结　　88
参考文献　　88
第10章　冗余和多样化　　89
10.1　冗余和多样化的历史　　89
10.2　标准中的冗余　　89
10.3　组件冗余还是系统冗余　　90
10.4　冗余　　91
10.4.1　系统冗余　　91
10.4.2　冷备用　　92
10.4.3　时间冗余　　93
10.5　多样化　　93
10.5.1　硬件多样化　　93
10.5.2　软件多样化　　94
10.5.3　数据多样化　　96
10.6　虚拟同步　　96
10.7　锁步处理器　　100
10.8　多样化监控器　　101
10.8.1　外部监控器模式　　101
10.8.2　看门狗式多样化监控器　　102
10.9　总结　　103
参考文献　　103
第四部分　设计验证
第11章　马尔可夫模型　　106
11.1　马尔可夫模型简介　　106
11.2　马尔可夫模型及相关标准　　106
11.3　马尔可夫假设　　107
11.4　计算示例　　108
11.4.1　估计比率　　108
11.4.2　识别系统状态　　109
11.4.3　建立方程式　　109
11.4.4　求解方程式　　110
11.4.5　分析结果　　110
11.5　马尔可夫模型的优势与劣势　　111
参考文献　　111
第12章　故障树　　112
12.1　FTA和FMECA　　112
12.2　标准中的故障树分析　　112
12.3　故障树类型　　113
12.4　示例1：布尔故障树　　113
12.5　示例2：扩展布尔故障树　　115
12.6　示例3：贝叶斯故障树　　115
12.6.1　噪声或　　117
12.6.2　从结果到原因的推理　　117
12.6.3　噪声与　　121
12.7　组合FTA　　121
12.8　FTA工具　　121
12.9　总结　　122
参考文献　　122
第13章　软件失效率　　123
13.1　潜在的异端邪说　　123
13.2　编译器和硬件效果　　124
13.3　评估失效率　　125
13.3.1　硬件失效率　　125
13.3.2　软件失效率　　126
13.4　失效建模　　126
13.5　示例公司　　130
参考文献　　130
第14章　半形式化设计验证　　132
14.1　重建设计的验证　　132
14.2　离散事件仿真　　133
14.2.1　离散事件仿真及其
标准　　134
14.2.2　伪随机数生成　　134
14.2.3　确定性系统的仿真　　135
14.2.4　不确定性系统的仿真　　136
14.2.5　离散事件仿真框架　　136
14.2.6　离散事件仿真示例　　137
14.2.7　知道何时开始　　139
14.2.8　知道何时停止　　139
14.3　时间Petri网　　139
14.3.1　Petri网及其标准　　139
14.3.2　Petri网的历史　　139
14.3.3　什么是Petri网　　140
14.3.4　一个简单的Petri网　　140
14.3.5　简单Petri网的扩展　　141
14.3.6　时间和随机Petri网　　142
14.3.7　理发店　　142
14.3.8　Petri网和马尔可夫
模型　　144
14.3.9　令牌代表什么　　145
14.3.10　着色网　　145
14.3.11　Petri网与非确定性　　145
14.3.12　Petri网习语　　146
14.4　仿真和示例公司　　146
参考文献　　147
第15章　形式化设计验证　　148
15.1　什么是形式化方法　　148
15.2　形式化方法的历史　　148
15.3　形式化方法和标准　　149
15.3.1　IEC 61508标准　　149
15.3.2　ISO 26262标准　　150
15.3.3　IEC 62304标准　　150
15.4　形式化方法有效吗　　151
15.5　形式化方法的类型　　152
15.6　自动代码和测试生成　　152
15.7　Spin建模工具　　153
15.7.1　Spin的历史记录　　153
15.7.2　Spin的结构　　153
15.7.3　Promela语言　　154
15.7.4　使用Spin检查互斥
算法　　154
15.7.5　Spin与线性时序逻辑　　155
15.7.6　Spin总结　　156
15.8　Rodin建模工具　　157
15.8.1　Rodin的历史　　157
15.8.2　Rodin的结构　　157
15.8.3　使用Rodin　　158
15.8.4　Rodin定理的证明　　159
15.8.5　再次检查互斥算法　　160
15.9　示例公司的形式化建模　　161
15.10　形式化方法：总结　　162
参考文献　　162
第五部分　编码
第16章　编码指南　　166
16.1　编程语言的选择　　166
16.2　与编程语言相关的标准　　166
16.3　语言特性　　167
16.3.1　定义的完整性　　167
16.3.2　明确的可信度支持　　 167
16.3.3　时间可预测性　　167
16.3.4　异常处理　　168
16.3.5　对静态检查的适应性　　168
16.3.6　大规模现场使用　　168
16.3.7　强类型指定和动态类型
指定　　 169
16.3.8　手误的检知　　170
16.3.9　函数式语言　　170
16.4　语言子集的使用　　170
16.5　那么，最好的编程语言是
什么　　171
16.6　浮点编程　　171
参考文献　　172
第17章　代码覆盖率度量　　173
17.1　代码覆盖率测试　　173
17.2　代码覆盖率的类型　　173
17.2.1　入口点覆盖率　　173
17.2.2　语句覆盖率　　173
17.2.3　分支覆盖率　　174
17.2.4　MC/DC覆盖率　　174
17.2.5　基础路径覆盖率　　175
17.2.6　路径覆盖率　　177
17.3　覆盖率及其标准　　177
17.4　覆盖率测试的有效性　　178
17.5　覆盖率的达成　　179
17.6　总结　　179
参考文献　　180
第18章　静态分析　　181
18.1　静态分析要做些什么　　181
18.2　静态代码分析及其标准　　182
18.3　静态代码分析　　182
18.3.1　语法级检查　　183
18.3.2　语法检查的语义增强　　184
18.3.3　故障密度评估　　186
18.3.4　通过不变量进行正确性
证明　　186
18.4　符号执行　　187
18.4.1　符号执行的优势　　187
18.4.2　符号执行及其标准　　188
18.4.3　符号执行工具KLEE　　188
18.5　总结　　189
参考文献　　189
第六部分　验证
第19章　集成测试　　192
19.1　故障注入测试　　192
19.1.1　为什么要注入故障　　192
19.1.2　向何处注入故障　　194
19.1.3　注入什么类型的故障　　195
19.1.4　故障注入及其标准　　195
19.1.5　ADC、BCI和故障
注入　　195
19.2　模型和代码间的背靠背测试
比较　　196
19.2.1　标准　　196
19.2.2　背靠背实例　　196
19.2.3　背靠背测试被使用
了吗　　197
19.2.4　当模型成为测试预言　　197
19.3　组合测试　　198
19.4　基于需求的测试　　201
19.4.1　安全需求是什么　　201
19.4.2　我们是否知晓全部
需求　　202
19.4.3　人的因素　　202
19.4.4　ISO 29119与基于需求的
测试　　202
19.5　集成测试过程中的异常检测　　203
参考文献　　203
第20章　工具链　　205
20.1　工具链的验证　　205
20.2　工具的分类　　205
20.3　BCI公司的工具分类　　206
20.4　使用第三方工具　　206
20.5　验证编译器　　207
20.5.1　多编译器法　　207
20.5.2　NPL法　　208
20.5.3　编译验证法　　209
20.6　ADC公司和BCI公司对
编译器的验证　　212
参考文献　　213
第21章　结论　　214
附录A　目标结构表示法　　215
附录B　贝叶斯信念网络　　219
附录C　计算（2+3）+4　　228
附录D　符号　　231