Available:*
Library | Item Barcode | Call Number | Material Type | Item Category 1 | Status |
---|---|---|---|---|---|
Searching... | 30000010197263 | QA76.76.R44 C68 2008 | Open Access Book | Book | Searching... |
On Order
Summary
Summary
Safety is a paradoxical system property. It remains immaterial, intangible and invisible until a failure, an accident or a catastrophy occurs and, too late, reveals its absence. And yet, a system cannot be relied upon unless its safety can be explained, demonstrated and certified. The practical and difficult questions which motivate this study concern the evidence and the arguments needed to justify the safety of a computer based system, or more generally its dependability. Dependability is a broad concept integrating properties such as safety, reliability, availability, maintainability and other related characteristics of the behaviour of a system in operation. How can we give the users the assurance that the system enjoys the required dependability? How should evidence be presented to certification bodies or regulatory authorities? What best practices should be applied? How should we decide whether there is enough evidence to justify the release of the system? To help answer these daunting questions, a method and a framework are proposed for the justification of the dependability of a computer-based system. The approach specifically aims at dealing with the difficulties raised by the validation of software. Hence, it should be of wide applicability despite being mainly based on the experience of assessing Nuclear Power Plant instrumentation and control systems important to safety. To be viable, a method must rest on a sound theoretical background.
Author Notes
Pierre-Jacques Courtois is a professor of computer science in the engineering department of the Catholic University of Louvain-la-Neuve in Belgium. He has degrees in electrical engineering and nuclear physics, and a doctorate in applied sciences. Formerly with the Philips Research Laboratory in Brussels, he has been working for the last fifteen years at the Belgian authorized inspection agency for nuclear installations, where he is in charge of the assessment of safety critical software based systems used in nuclear power plants. He has served as a consultant to the OECD and to the IAEA for issuing guidance on the design and validation of software important to nuclear safety. He has also served as the chairman of the European Commission nuclear regulator task force on licensing issues of nuclear safety critical software, and he has been active in several European research projects on dependable computer systems and nuclear safety.
Table of Contents
Part I The Context | |
1 Introduction | p. 3 |
2 Current Practices | p. 9 |
3 Axiomatic Justification and Uncertainty | p. 13 |
4 Justification and Dependability Case | p. 17 |
4.1 Cost Minimization and the Proportionality Principle | p. 18 |
4.2 Risk-based Assessment | p. 19 |
4.3 Two Illustrative Case Studies: A Process Instrumentation (SIP) and a Radioactive Materials Handling System | p. 19 |
Part II Prescriptions | |
5 Requirements, Claims and Evidence | p. 23 |
5.1 Where to Start? The First Foundation of Dependability Justification | p. 23 |
5.2 The Initial Dependability Requirements (CLM0) | p. 24 |
5.2.1 PIE's, Constraints, Safe States | p. 25 |
5.2.2 Elicitation | p. 26 |
5.2.3 Completeness | p. 27 |
5.3 The Other Foundation: The System Input-Output Preliminary Requirements | p. 28 |
5.4 Primary Claims | p. 29 |
5.5 Differences Between Dependability Requirements and Claims | p. 30 |
5.6 Evidence and Model Assumptions | p. 32 |
5.7 How to Organize Evidence? A Four-level Structure | p. 33 |
5.8 How Are the Four Levels Related? Levels of Causality | p. 36 |
5.9 Examples | p. 39 |
6 Arguments, Syntax and Semantics | p. 41 |
6.1 Claim Assertions | p. 41 |
6.2 White, Grey and Black Claims | p. 42 |
6.3 The Inductive Justification Process | p. 43 |
6.4 The Conjunctive Property | p. 46 |
6.5 The Syntax of an Argument | p. 49 |
6.5.1 Delegations and Expansions | p. 49 |
6.5.2 Claim Justifications | p. 50 |
6.5.3 Argument Unicity and Termination | p. 51 |
6.6 Claim and Argument Semantic Aspects | p. 52 |
6.6.1 Delegation and Expansion as Tools for Refinement of Evidence and Argument Incremental Construction | p. 52 |
6.6.2 Universal and Existential Claim Assertions | p. 54 |
6.6.3 Claim Refutation | p. 56 |
6.6.4 Absence of Level-1 Grey Primary Claims | p. 56 |
6.6.5 Adjacent Delegation Sub-claims | p. 56 |
7 Axiomatic Principles and Limits | p. 59 |
7.1 Claim Justifiability | p. 59 |
7.2 Evidence Plausibility and Weight | p. 61 |
7.3 The Ineluctability of Consensus | p. 62 |
7.4 Epistemic Versus Stochastic Uncertainty | p. 64 |
7.5 Claims on Product Versus Evidence from Process | p. 67 |
7.6 Logics of Prevention, Precaution and Enlightened Catastrophism | p. 68 |
7.7 Concluding Remarks on Claims, Arguments, Evidence | p. 69 |
Part III Descriptions | |
8 Structures and Interpretations | p. 73 |
8.1 The Roles of Models in Dependability Assessment | p. 74 |
8.2 Basic Model Notions | p. 75 |
8.2.1 Model Structures and Relations | p. 76 |
8.2.2 Predicates | p. 78 |
8.2.3 Languages and Proofs | p. 79 |
8.3 On Descriptions and Interpretations | p. 79 |
8.4 Mathematical Structures | p. 81 |
8.5 System Structures | p. 82 |
8.6 L-Interpretations | p. 84 |
8.7 The Formal Definition of a Model | p. 85 |
8.8 Validation and Satisfiability Obligations | p. 86 |
8.8.1 Language Expansion/Reduction | p. 86 |
8.8.2 Substructures and Extensions | p. 87 |
8.8.3 L[subscript 1]-Interpretation (Environment-System Interface) | p. 90 |
8.8.4 L[subscript i]-Interpretations (i = 2, 3, 4) | p. 96 |
8.9 Interdependencies Between Structures of Different Levels | p. 100 |
8.9.1 Properties of Justification Structures | p. 100 |
8.9.2 Properties of Expansion Structures | p. 104 |
8.9.3 Internal Compound Structure and Interfaces of a Level-i, i = 1...4 | p. 107 |
8.10 Interdependencies Between Languages of Different Levels | p. 107 |
8.11 The Tree of Sub-structures Dependencies | p. 110 |
8.12 A General Multi-level Justification Framework | p. 111 |
8.13 Design Abstractions | p. 112 |
8.14 Recommendations for Design and Validation Models | p. 113 |
9 Embedded Computer System Structures | p. 117 |
9.1 States, Events and Other Basic Notions | p. 118 |
9.2 Notation | p. 120 |
9.3 Level-0. Environment Requirements, Events and Constraints | p. 121 |
9.3.1 CLM0 Dependability Requirements | p. 121 |
9.3.2 CLM0 Postulated Initiating Events and Safe Failure Modes | p. 122 |
9.3.3 CLM0 Environment Constraints | p. 122 |
9.3.4 Level-0 Dependability Case Documentation | p. 122 |
9.4 Level-1. System-Environment Interface | p. 123 |
9.4.1 Selection of the Entities and Relations of the Interface | p. 123 |
9.4.2 Environment States | p. 124 |
9.4.3 Constraints (NAT) | p. 125 |
9.4.4 A Note on Environment Assumptions | p. 126 |
9.4.5 Postulated Initiating Events (Relation HAZ[superscript 1]) | p. 126 |
9.4.6 System Input-Output Preliminary Specifications | p. 127 |
9.4.7 The System and the Functional Relation (REQ) | p. 128 |
9.4.8 The Need for a Unique Interpretation for Requirements and System Specifications | p. 128 |
9.4.9 Expansion of the CLM0 Requirements into Primary Claims | p. 129 |
9.4.10 Primary Validity Claim-Justification Substructures | p. 130 |
9.4.11 Implementation Primary Claims - Justification Structures | p. 137 |
9.4.12 Primary Dependability Claims - Justification Substructures | p. 139 |
9.4.13 Level-1 CLM0 Expansion Structure | p. 144 |
9.4.14 Level-1 Evidence and Delegation Claims | p. 147 |
9.4.15 Level-1 Argument | p. 149 |
9.4.16 Level-1 Documentation | p. 150 |
9.5 Level-2. Computer System Architecture | p. 151 |
9.5.1 Elements of the Architecture | p. 152 |
9.5.2 Input and Output Variables | p. 152 |
9.5.3 Channel k Data Acquisition (Relations IN[subscript k]) | p. 153 |
9.5.4 Channel Assignment Relation (IN) | p. 154 |
9.5.5 Channel k Output Device (Relations OUT[subscript k]) | p. 154 |
9.5.6 Voting Relations (OUT) | p. 155 |
9.5.7 Channel k Requirements (REQ[subscript k]) | p. 155 |
9.5.8 Level-2 Undesired Events (HAZ[superscript 2]) | p. 156 |
9.5.9 Level-2 Expansion of Level-1 Delegation Claims | p. 158 |
9.5.10 Expansion of REQ Acceptable Implementation Delegation Claim[1,2] | p. 158 |
9.5.11 Expansion of REQ Fail-Safe Implementation Delegation Claim[1,2] | p. 164 |
9.5.12 Expansion of Functional Diversity Delegation Claim[1,2] | p. 169 |
9.5.13 Expansion of Reliability and Safety Delegation Claims[1,2] | p. 175 |
9.5.14 Level-2 Expansions | p. 182 |
9.5.15 Level-2 Evidence and Delegation Claims | p. 183 |
9.5.16 A Digression on Testing | p. 184 |
9.5.17 Level-2 Argument | p. 184 |
9.5.18 Level-2 Documentation | p. 185 |
9.6 Level-3. Design | p. 187 |
9.6.1 Complexity and Elements of the Design | p. 187 |
9.6.2 The Design Relations (SOF[subscript k]) | p. 187 |
9.6.3 Design Level Undesired Events | p. 189 |
9.6.4 Level-3 Expansion of Level-2 Delegation Claims | p. 191 |
9.6.5 Expansion of Channel Acceptable Implementation Delegation Claim[2,3] | p. 191 |
9.6.6 Expansion of Channel Fail-Safe Implementation Claim[2,3] | p. 196 |
9.6.7 Expansion of Channel Independency Delegation Claim[2,3] | p. 199 |
9.6.8 Expansion of Reliability and Safety Delegation Claims[2,3] | p. 206 |
9.6.9 Level-3 Expansions | p. 210 |
9.6.10 Level-3 Evidence and Delegation Claims | p. 211 |
9.6.11 Level-3 Argument | p. 214 |
9.6.12 Level-3 Documentation | p. 215 |
9.7 Structure of the Operation Control | p. 216 |
9.7.1 Elements of the Operation Control Structure | p. 218 |
9.7.2 Operation Control Relations READ[subscript k] and ORDER[subscript k] | p. 219 |
9.7.3 Control of Operation. Undesired Events (HAZ[superscript 4]) | p. 219 |
9.7.4 Level-4 Expansion of Level-3 Delegation Claims | p. 220 |
9.7.5 Expansion of Accuracy Delegation Claim[2,4] | p. 220 |
9.7.6 Expansion of Channel Fail-safe Control Delegation Claim[3,4] | p. 224 |
9.7.7 Expansion of Channel Reliability and Safety Delegation Claims[2,4] | p. 229 |
9.7.8 Level-4 Expansion | p. 234 |
9.7.9 Level-4 Evidence | p. 236 |
9.7.10 Level-4 Argument | p. 236 |
9.7.11 Level-4 Dependability Case Documentation | p. 237 |
9.8 Guidance Provided by the System Substructure Tree | p. 238 |
9.9 Concluding Remarks: Model Inter-relations and Preservation Properties | p. 239 |
Part IV Methodological Implications | |
10 Pre-existing Systems and Components | p. 245 |
10.1 Pre-existing Components | p. 246 |
10.2 Composability and Re-use of Arguments | p. 246 |
10.2.1 Syntactical Conditions | p. 247 |
10.2.2 Semantic Conditions | p. 247 |
10.3 Guaranteed Services and Rely Conditions | p. 248 |
10.4 The System-Component Interface Substructures | p. 250 |
10.4.1 The GRANT and RELY Relations | p. 250 |
10.4.2 The HAZ[superscript s] Relation | p. 251 |
10.4.3 Proof Obligations for the Developer of S | p. 252 |
10.4.4 The U[subscript s]([delta xi subscript s]) Expansion Structures | p. 254 |
10.4.5 Proof Obligations for the Embedding System | p. 255 |
10.4.6 System-Component Interface Revisited | p. 262 |
10.5 Documentation | p. 263 |
10.6 Concluding Remarks and Justification Issues | p. 265 |
10.6.1 Completeness of S Specifications | p. 265 |
10.6.2 Robustness of S Operation | p. 267 |
10.7 Criticality Degrees and Integrity Levels | p. 268 |
11 Construction Methods | p. 269 |
11.1 Dependability Case Construction Rules | p. 269 |
11.1.1 Initial Dependability Requirements Address Product, Not Process Quality Assurance | p. 269 |
11.1.2 A Unique Interpretation Model for the Specification of Initial Dependability Requirements and for the Validation of Preliminary Specifications | p. 270 |
11.1.3 Expansions | p. 270 |
11.1.4 Claims First | p. 271 |
11.1.5 Expansion and Justification Interpretation Structures | p. 271 |
11.1.6 Ordering for Claim Elicitation and Justification | p. 272 |
11.1.7 Primary Claims | p. 273 |
11.1.8 Level-1 Expansion | p. 273 |
11.1.9 Assumptions Are Not Evidence | p. 274 |
11.1.10 Evidence Must Be Explicitly Claimed | p. 274 |
11.1.11 Claim Identification and Documentation | p. 275 |
11.1.12 Fixed Levels of Expansion and Evidence | p. 275 |
11.1.13 Strict Conjunctions | p. 276 |
11.1.14 Delegation to the Adjacent Lower Evidence Level | p. 276 |
11.1.15 Re-use of Arguments | p. 276 |
11.1.16 Pre-existing Components | p. 278 |
11.2 FFP (Functions/Failures/Properties) Method | p. 278 |
12 Postface | p. 283 |
A The SIP System | p. 287 |
A.1 Description | p. 287 |
A.2 Plant, Technology and Safety Replacement Constraints | p. 289 |
A.3 Dependability Requirements (CLM0) and Primary Claims | p. 290 |
A.4 Primary Claims on Software CCF's | p. 291 |
A.5 Software Architecture and Design. Claims and Evidence | p. 292 |
A.5.1 Operating System | p. 292 |
A.5.2 Library Modules | p. 292 |
A.5.3 Application Software | p. 293 |
B Automated Material Handling System | p. 295 |
B.1 Description | p. 295 |
B.2 Dependability Requirements (CLM0) | p. 296 |
B.3 Constraints and Postulated Initiating Events | p. 298 |
B.4 Preliminary Specifications and Primary Claims | p. 298 |
References | p. 309 |
Index | p. 317 |