Foreword |
|
xiii | |
Preface |
|
xv | |
|
|
1 | (26) |
|
1.1 The Elements of Dependability |
|
|
1 | (4) |
|
|
1 | (3) |
|
|
4 | (1) |
|
1.2 The Role of the Software Engineer |
|
|
5 | (2) |
|
1.3 Our Dependence on Computers |
|
|
7 | (2) |
|
1.4 Some Regrettable Failures |
|
|
9 | (4) |
|
|
9 | (1) |
|
1.4.2 Korean Air Flight 801 |
|
|
10 | (1) |
|
1.4.3 The Mars Climate Orbiter |
|
|
11 | (1) |
|
1.4.4 The Mars Polar Lander |
|
|
11 | (1) |
|
1.4.5 Other Important Incidents |
|
|
12 | (1) |
|
1.4.6 How to Think about Failures |
|
|
12 | (1) |
|
1.5 Consequences of Failure |
|
|
13 | (4) |
|
1.5.1 Non-Obvious Consequences of Failure |
|
|
13 | (1) |
|
1.5.2 Unexpected Costs of Failure |
|
|
14 | (1) |
|
1.5.3 Categories of Consequences |
|
|
15 | (1) |
|
1.5.4 Determining the Consequences of Failure |
|
|
16 | (1) |
|
1.6 The Need for Dependability |
|
|
17 | (1) |
|
1.7 Systems and Their Dependability Requirements |
|
|
18 | (4) |
|
|
18 | (2) |
|
1.7.2 Systems That Help Build Systems |
|
|
20 | (1) |
|
1.7.3 Systems That Interact with Other Systems |
|
|
21 | (1) |
|
1.8 Where Do We Go from Here? |
|
|
22 | (1) |
|
1.9 Organization of This Book |
|
|
23 | (4) |
|
|
25 | (2) |
|
Chapter 2 Dependability Requirements |
|
|
27 | (46) |
|
2.1 Why We Need Dependability Requirements |
|
|
27 | (1) |
|
2.2 The Evolution of Dependability Concepts |
|
|
28 | (2) |
|
2.3 The Role of Terminology |
|
|
30 | (1) |
|
|
31 | (3) |
|
2.5 Requirements and Specification |
|
|
34 | (1) |
|
|
35 | (6) |
|
2.6.1 The Notion of Service Failure |
|
|
35 | (1) |
|
2.6.2 Sources of Service Failure |
|
|
36 | (2) |
|
2.6.3 A Practical View of Requirements and Specification |
|
|
38 | (1) |
|
2.6.4 Viewpoints of Service Failure |
|
|
39 | (1) |
|
2.6.5 Informing the User about Failure |
|
|
40 | (1) |
|
2.7 Dependability and Its Attributes |
|
|
41 | (14) |
|
|
43 | (1) |
|
|
44 | (4) |
|
|
48 | (1) |
|
|
48 | (3) |
|
|
51 | (1) |
|
|
52 | (1) |
|
|
53 | (1) |
|
2.7.8 A Word about Security |
|
|
53 | (1) |
|
2.7.9 The Notion of Trust |
|
|
54 | (1) |
|
2.8 Systems, Software, and Dependability |
|
|
55 | (3) |
|
2.8.1 Computers Are neither Unsafe nor Insecure |
|
|
55 | (1) |
|
2.8.2 Why Application System Dependability? |
|
|
55 | (1) |
|
2.8.3 Application System Dependability and Computers |
|
|
56 | (2) |
|
2.9 Defining Dependability Requirements |
|
|
58 | (7) |
|
2.9.1 A First Example, an Automobile Cruise Control |
|
|
60 | (1) |
|
2.9.2 A Second Example, a Pacemaker |
|
|
61 | (4) |
|
2.10 As Low As is Reasonably Practicable ALARP |
|
|
65 | (8) |
|
2.10.1 The Need for ALARP |
|
|
65 | (1) |
|
|
66 | (1) |
|
2.10.3 ALARP Carrot Diagrams |
|
|
67 | (2) |
|
|
69 | (4) |
|
Chapter 3 Errors, Faults, and Hazards |
|
|
73 | (30) |
|
|
73 | (2) |
|
3.2 The Complexity of Erroneous States |
|
|
75 | (1) |
|
3.3 Faults and Dependability |
|
|
76 | (3) |
|
3.3.1 Definition of Fault |
|
|
76 | (2) |
|
|
78 | (1) |
|
|
78 | (1) |
|
3.3.4 Achieving Dependability |
|
|
78 | (1) |
|
3.4 The Manifestation of Faults |
|
|
79 | (1) |
|
|
80 | (4) |
|
3.5.1 Degradation Fault Probabilities --- The "Bathtub" Curve |
|
|
80 | (1) |
|
3.5.2 An Example of Degradation Faults --- Hard Disks |
|
|
81 | (3) |
|
|
84 | (1) |
|
|
85 | (4) |
|
|
85 | (1) |
|
3.7.2 An Example Byzantine Fault |
|
|
86 | (2) |
|
3.7.3 Nuances of Byzantine Faults |
|
|
88 | (1) |
|
3.8 Component Failure Semantics |
|
|
89 | (2) |
|
|
89 | (1) |
|
3.8.2 Achieving Predictable Failure Semantics |
|
|
90 | (1) |
|
3.8.3 Software Failure Semantics |
|
|
90 | (1) |
|
3.9 Fundamental Principle of Dependability |
|
|
91 | (2) |
|
|
92 | (1) |
|
|
92 | (1) |
|
|
92 | (1) |
|
|
93 | (1) |
|
|
93 | (1) |
|
|
94 | (3) |
|
3.11.1 The Hazard Concept |
|
|
94 | (1) |
|
3.11.2 Hazard Identification |
|
|
95 | (1) |
|
3.11.3 Hazards and Faults |
|
|
96 | (1) |
|
3.12 Engineering Dependable Systems |
|
|
97 | (6) |
|
|
100 | (3) |
|
Chapter 4 Dependability Analysis |
|
|
103 | (20) |
|
|
103 | (1) |
|
4.2 Generalizing the Notion of Hazard |
|
|
104 | (1) |
|
|
105 | (12) |
|
4.3.1 Basic Concept of a Fault Tree |
|
|
105 | (1) |
|
4.3.2 Basic and Compound Events |
|
|
106 | (2) |
|
4.3.3 Inspection of Fault Trees |
|
|
108 | (1) |
|
4.3.4 Probabilistic Fault Tree Analysis |
|
|
108 | (1) |
|
4.3.5 Software and Fault Trees |
|
|
109 | (2) |
|
4.3.6 An Example Fault Tree |
|
|
111 | (2) |
|
|
113 | (3) |
|
4.3.8 Other Applications of Fault Trees |
|
|
116 | (1) |
|
4.4 Failure Modes, Effects, and Criticality Analysis |
|
|
117 | (2) |
|
|
117 | (2) |
|
4.5 Hazard and Operability Analysis |
|
|
119 | (4) |
|
4.5.1 The Concept of HazOp |
|
|
119 | (1) |
|
4.5.2 The Basic HazOp Process |
|
|
120 | (1) |
|
4.5.3 HazOp and Computer Systems |
|
|
120 | (2) |
|
|
122 | (1) |
|
Chapter 5 Dealing with Faults |
|
|
123 | (24) |
|
5.1 Faults and Their Treatment |
|
|
123 | (1) |
|
|
124 | (2) |
|
|
124 | (1) |
|
|
125 | (1) |
|
|
126 | (1) |
|
|
126 | (1) |
|
|
126 | (1) |
|
|
127 | (6) |
|
5.4.1 Familiarity with Fault Tolerance |
|
|
127 | (1) |
|
|
127 | (2) |
|
5.4.3 Semantics of Fault Tolerance |
|
|
129 | (1) |
|
5.4.4 Phases of Fault Tolerance |
|
|
130 | (1) |
|
5.4.5 An Example Fault-Tolerant System |
|
|
131 | (2) |
|
|
133 | (4) |
|
5.5.1 Fault Forecasting Process |
|
|
134 | (1) |
|
5.5.2 The Operating Environment |
|
|
134 | (1) |
|
|
135 | (1) |
|
|
135 | (2) |
|
5.6 Applying the Four Approaches to Fault Treatment |
|
|
137 | (1) |
|
5.7 Dealing with Byzantine Faults |
|
|
137 | (10) |
|
5.7.1 The Byzantine Generals |
|
|
138 | (1) |
|
5.7.2 The Byzantine Generals and Computers |
|
|
139 | (2) |
|
5.7.3 The Impossibility Result |
|
|
141 | (2) |
|
5.7.4 Solutions to the Byzantine Generals Problem |
|
|
143 | (2) |
|
|
145 | (2) |
|
Chapter 6 Degradation Faults and Software |
|
|
147 | (34) |
|
|
147 | (1) |
|
|
148 | (5) |
|
6.2.1 Redundancy and Replication |
|
|
148 | (3) |
|
6.2.2 Large vs. Small Component Redundancy |
|
|
151 | (1) |
|
6.2.3 Static vs. Dynamic Redundancy |
|
|
152 | (1) |
|
6.3 Redundant Architectures |
|
|
153 | (15) |
|
|
155 | (3) |
|
6.3.2 Switched Dual Redundancy |
|
|
158 | (6) |
|
6.3.3 N-Modular Redundancy |
|
|
164 | (2) |
|
|
166 | (2) |
|
6.4 Quantifying the Benefits of Redundancy |
|
|
168 | (2) |
|
6.4.1 Statistical Independence |
|
|
168 | (1) |
|
6.4.2 Dual-Redundant Architecture |
|
|
169 | (1) |
|
6.5 Distributed Systems and Fail-Stop Computers |
|
|
170 | (11) |
|
6.5.1 Distributed Systems |
|
|
170 | (1) |
|
6.5.2 Failure Semantics of Computers |
|
|
171 | (1) |
|
6.5.3 Exploiting Distributed Systems |
|
|
172 | (1) |
|
6.5.4 The Fail-Stop Concept |
|
|
172 | (2) |
|
6.5.5 Implementing Fail-Stop Computers |
|
|
174 | (1) |
|
6.5.6 Programming Fail-Stop Computers |
|
|
175 | (3) |
|
|
178 | (3) |
|
Chapter 7 Software Dependability |
|
|
181 | (40) |
|
7.1 Faults and the Software Lifecycle |
|
|
181 | (5) |
|
7.1.1 Software and Its Fragility |
|
|
182 | (1) |
|
7.1.2 Dealing with Software Faults |
|
|
183 | (1) |
|
7.1.3 The Software Lifecycle |
|
|
184 | (1) |
|
7.1.4 Verification and Validation |
|
|
185 | (1) |
|
|
186 | (4) |
|
7.2.1 Analysis in Software Engineering |
|
|
186 | (3) |
|
7.2.2 Formal Specification |
|
|
189 | (1) |
|
7.2.3 Formal Verification |
|
|
189 | (1) |
|
7.2.4 The Terminology of Correctness |
|
|
190 | (1) |
|
7.3 Verification by Model Checking |
|
|
190 | (3) |
|
7.3.1 The Role of Model Checking |
|
|
190 | (1) |
|
|
191 | (1) |
|
7.3.3 Using a Model Checker |
|
|
192 | (1) |
|
7.4 Correctness by Construction |
|
|
193 | (1) |
|
7.5 Approaches to Correctness by Construction |
|
|
194 | (3) |
|
7.6 Correctness by Construction --- Synthesis |
|
|
197 | (4) |
|
7.6.1 Generating Code from Formal Specifications |
|
|
197 | (1) |
|
7.6.2 The Advantages of Model-Based Development |
|
|
198 | (1) |
|
7.6.3 Examples of Model-Based Development Systems |
|
|
199 | (1) |
|
7.6.4 Mathworks Simulink® |
|
|
200 | (1) |
|
7.7 Correctness by Construction --- Refinement |
|
|
201 | (2) |
|
7.8 Software Fault Avoidance |
|
|
203 | (4) |
|
7.8.1 Rigorous Development Processes |
|
|
204 | (1) |
|
7.8.2 Appropriate Notations |
|
|
205 | (1) |
|
7.8.3 Comprehensive Standards for All Artifacts |
|
|
206 | (1) |
|
|
207 | (1) |
|
7.8.5 Properly Trained Personnel |
|
|
207 | (1) |
|
|
207 | (1) |
|
7.9 Software Fault Elimination |
|
|
207 | (5) |
|
|
208 | (1) |
|
|
209 | (1) |
|
7.9.3 Eliminating a Fault --- Root-Cause Analysis |
|
|
210 | (2) |
|
7.10 Managing Software Fault Avoidance and Elimination |
|
|
212 | (3) |
|
7.10.1 Fault Freedom as Properties |
|
|
212 | (3) |
|
7.11 Misconceptions about Software Dependability |
|
|
215 | (6) |
|
|
218 | (3) |
|
Chapter 8 Software Fault Avoidance in Specification |
|
|
221 | (36) |
|
8.1 The Role of Specification |
|
|
221 | (1) |
|
8.2 Difficulties with Natural Languages |
|
|
222 | (1) |
|
8.3 Specification Difficulties |
|
|
223 | (3) |
|
8.3.1 Specification Defects |
|
|
223 | (1) |
|
8.3.2 Specification Evolution |
|
|
224 | (2) |
|
|
226 | (8) |
|
8.4.1 Formal Syntax and Semantics |
|
|
226 | (2) |
|
8.4.2 Benefits of Formal Languages |
|
|
228 | (2) |
|
8.4.3 Presentation of Formal Languages |
|
|
230 | (1) |
|
8.4.4 Types of Formal Languages |
|
|
231 | (1) |
|
8.4.5 Discrete Mathematics and Formal Specification |
|
|
232 | (1) |
|
8.4.6 The Before and After State |
|
|
232 | (1) |
|
8.4.7 A Simple Specification Example |
|
|
233 | (1) |
|
8.5 Model-Based Specification |
|
|
234 | (3) |
|
8.5.1 Using a Model-Based Specification |
|
|
235 | (2) |
|
8.6 The Declarative Language Z |
|
|
237 | (7) |
|
|
237 | (1) |
|
8.6.2 Propositions and Predicates |
|
|
238 | (2) |
|
|
240 | (1) |
|
|
241 | (1) |
|
8.6.5 Relations, Sequences, and Functions |
|
|
241 | (1) |
|
|
242 | (1) |
|
8.6.7 The Schema Calculus |
|
|
243 | (1) |
|
|
244 | (1) |
|
|
245 | (7) |
|
8.8.1 Version 1 of the Example |
|
|
247 | (1) |
|
8.8.2 Version 2 of the Example |
|
|
248 | (1) |
|
8.8.3 Version 3 of the Example |
|
|
248 | (3) |
|
8.8.4 Version 4 of the Example |
|
|
251 | (1) |
|
8.9 Overview of Formal Specification Development |
|
|
252 | (5) |
|
|
254 | (3) |
|
Chapter 9 Software Fault Avoidance in Implementation |
|
|
257 | (34) |
|
9.1 Implementing Software |
|
|
257 | (4) |
|
9.1.1 Tool Support for Software Implementation |
|
|
258 | (1) |
|
9.1.2 Developing an Implementation |
|
|
258 | (1) |
|
9.1.3 What Goes Wrong with Software? |
|
|
259 | (2) |
|
9.2 Programming Languages |
|
|
261 | (3) |
|
9.2.1 The C Programming Language |
|
|
262 | (2) |
|
|
264 | (6) |
|
9.3.1 The Motivation for Ada |
|
|
264 | (1) |
|
|
265 | (3) |
|
|
268 | (1) |
|
9.3.4 Concurrent and Real-Time Programming |
|
|
268 | (1) |
|
9.3.5 Separate Compilation |
|
|
269 | (1) |
|
|
270 | (1) |
|
9.4 Programming Standards |
|
|
270 | (3) |
|
9.4.1 Programming Standards and Programming Languages |
|
|
270 | (2) |
|
9.4.2 Programming Standards and Fault Avoidance |
|
|
272 | (1) |
|
9.5 Correctness by Construction --- SPARK |
|
|
273 | (18) |
|
9.5.1 The SPARK Development Concept |
|
|
274 | (2) |
|
9.5.2 The SPARK Ada Subset |
|
|
276 | (2) |
|
9.5.3 The SPARK Annotations |
|
|
278 | (1) |
|
|
278 | (3) |
|
|
281 | (2) |
|
|
283 | (4) |
|
|
287 | (2) |
|
|
289 | (2) |
|
Chapter 10 Software Fault Elimination |
|
|
291 | (28) |
|
10.1 Why Fault Elimination? |
|
|
291 | (2) |
|
|
293 | (10) |
|
10.2.1 Artifacts and Defects |
|
|
293 | (2) |
|
|
295 | (3) |
|
|
298 | (1) |
|
10.2.4 Phased Inspections |
|
|
299 | (4) |
|
|
303 | (16) |
|
10.3.1 Exhaustive Testing |
|
|
303 | (1) |
|
10.3.2 The Role of Testing |
|
|
304 | (1) |
|
10.3.3 The Testing Process |
|
|
305 | (2) |
|
|
307 | (1) |
|
|
308 | (1) |
|
|
309 | (2) |
|
10.3.7 Modified Condition Decision Coverage |
|
|
311 | (2) |
|
|
313 | (1) |
|
|
314 | (3) |
|
|
317 | (2) |
|
Chapter 11 Software Fault Tolerance |
|
|
319 | (36) |
|
11.1 Components Subject to Design Faults |
|
|
319 | (2) |
|
11.2 Issues with Design Fault Tolerance |
|
|
321 | (5) |
|
11.2.1 The Difficulty of Tolerating Design Faults |
|
|
321 | (2) |
|
11.2.2 Self-Healing Systems |
|
|
323 | (1) |
|
|
324 | (1) |
|
11.2.4 Forward and Backward Error Recovery |
|
|
324 | (2) |
|
11.3 Software Replication |
|
|
326 | (1) |
|
|
327 | (12) |
|
|
328 | (3) |
|
|
331 | (2) |
|
11.4.3 Conversations and Dialogs |
|
|
333 | (1) |
|
11.4.4 Measuring Design Diversity |
|
|
334 | (1) |
|
11.4.5 Comparison Checking |
|
|
335 | (2) |
|
11.4.6 The Consistent Comparison Problem |
|
|
337 | (2) |
|
|
339 | (5) |
|
|
339 | (1) |
|
11.5.2 A Special Case of Data Diversity |
|
|
340 | (1) |
|
11.5.3 Generalized Data Diversity |
|
|
341 | (1) |
|
|
342 | (1) |
|
11.5.5 N-Copy Execution and Voting |
|
|
343 | (1) |
|
11.6 Targeted Fault Tolerance |
|
|
344 | (11) |
|
|
345 | (2) |
|
11.6.2 Application Isolation |
|
|
347 | (2) |
|
|
349 | (1) |
|
|
349 | (2) |
|
11.6.5 Execution Time Checking |
|
|
351 | (2) |
|
|
353 | (2) |
|
Chapter 12 Dependability Assessment |
|
|
355 | (38) |
|
12.1 Approaches to Assessment |
|
|
355 | (2) |
|
12.2 Quantitative Assessment |
|
|
357 | (5) |
|
12.2.1 The Basic Approach |
|
|
357 | (2) |
|
|
359 | (1) |
|
12.2.3 Compositional Modeling |
|
|
360 | (1) |
|
12.2.4 Difficulties with Quantitative Assessment |
|
|
361 | (1) |
|
12.3 Prescriptive Standards |
|
|
362 | (9) |
|
12.3.1 The Goal of Prescriptive Standards |
|
|
364 | (1) |
|
12.3.2 Example Prescriptive Standard --- RTCA/DO-178B |
|
|
364 | (5) |
|
12.3.3 The Advantages of Prescriptive Standards |
|
|
369 | (1) |
|
12.3.4 The Disadvantages of Prescriptive Standards |
|
|
370 | (1) |
|
|
371 | (17) |
|
12.4.1 The Concept of Argument |
|
|
372 | (1) |
|
|
373 | (2) |
|
12.4.3 Regulation Based on Safety Cases |
|
|
375 | (1) |
|
12.4.4 Building a Safety Case |
|
|
376 | (1) |
|
|
377 | (3) |
|
12.4.6 The Goal Structuring Notation |
|
|
380 | (2) |
|
12.4.7 Software and Arguments |
|
|
382 | (3) |
|
|
385 | (2) |
|
12.4.9 Safety Case Patterns |
|
|
387 | (1) |
|
12.5 Applicability of Argumentation |
|
|
388 | (5) |
|
|
391 | (2) |
Bibliography |
|
393 | (12) |
Index |
|
405 | |