安全關鍵系統嵌入式軟件開發指南

克裏斯·霍布斯（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