Skip to:Content
|
Bottom
Cover image for Justifying the dependability of computer-based aystems : with applications in nuclear engineering
Title:
Justifying the dependability of computer-based aystems : with applications in nuclear engineering
Personal Author:
Series:
Springer series in reliability engineering ;
Publication Information:
London, UK : Springer, 2008
Physical Description:
xviii, 323 p. : ill. ; 24 cm.
ISBN:
9781848003712

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 Introductionp. 3
2 Current Practicesp. 9
3 Axiomatic Justification and Uncertaintyp. 13
4 Justification and Dependability Casep. 17
4.1 Cost Minimization and the Proportionality Principlep. 18
4.2 Risk-based Assessmentp. 19
4.3 Two Illustrative Case Studies: A Process Instrumentation (SIP) and a Radioactive Materials Handling Systemp. 19
Part II Prescriptions
5 Requirements, Claims and Evidencep. 23
5.1 Where to Start? The First Foundation of Dependability Justificationp. 23
5.2 The Initial Dependability Requirements (CLM0)p. 24
5.2.1 PIE's, Constraints, Safe Statesp. 25
5.2.2 Elicitationp. 26
5.2.3 Completenessp. 27
5.3 The Other Foundation: The System Input-Output Preliminary Requirementsp. 28
5.4 Primary Claimsp. 29
5.5 Differences Between Dependability Requirements and Claimsp. 30
5.6 Evidence and Model Assumptionsp. 32
5.7 How to Organize Evidence? A Four-level Structurep. 33
5.8 How Are the Four Levels Related? Levels of Causalityp. 36
5.9 Examplesp. 39
6 Arguments, Syntax and Semanticsp. 41
6.1 Claim Assertionsp. 41
6.2 White, Grey and Black Claimsp. 42
6.3 The Inductive Justification Processp. 43
6.4 The Conjunctive Propertyp. 46
6.5 The Syntax of an Argumentp. 49
6.5.1 Delegations and Expansionsp. 49
6.5.2 Claim Justificationsp. 50
6.5.3 Argument Unicity and Terminationp. 51
6.6 Claim and Argument Semantic Aspectsp. 52
6.6.1 Delegation and Expansion as Tools for Refinement of Evidence and Argument Incremental Constructionp. 52
6.6.2 Universal and Existential Claim Assertionsp. 54
6.6.3 Claim Refutationp. 56
6.6.4 Absence of Level-1 Grey Primary Claimsp. 56
6.6.5 Adjacent Delegation Sub-claimsp. 56
7 Axiomatic Principles and Limitsp. 59
7.1 Claim Justifiabilityp. 59
7.2 Evidence Plausibility and Weightp. 61
7.3 The Ineluctability of Consensusp. 62
7.4 Epistemic Versus Stochastic Uncertaintyp. 64
7.5 Claims on Product Versus Evidence from Processp. 67
7.6 Logics of Prevention, Precaution and Enlightened Catastrophismp. 68
7.7 Concluding Remarks on Claims, Arguments, Evidencep. 69
Part III Descriptions
8 Structures and Interpretationsp. 73
8.1 The Roles of Models in Dependability Assessmentp. 74
8.2 Basic Model Notionsp. 75
8.2.1 Model Structures and Relationsp. 76
8.2.2 Predicatesp. 78
8.2.3 Languages and Proofsp. 79
8.3 On Descriptions and Interpretationsp. 79
8.4 Mathematical Structuresp. 81
8.5 System Structuresp. 82
8.6 L-Interpretationsp. 84
8.7 The Formal Definition of a Modelp. 85
8.8 Validation and Satisfiability Obligationsp. 86
8.8.1 Language Expansion/Reductionp. 86
8.8.2 Substructures and Extensionsp. 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 Levelsp. 100
8.9.1 Properties of Justification Structuresp. 100
8.9.2 Properties of Expansion Structuresp. 104
8.9.3 Internal Compound Structure and Interfaces of a Level-i, i = 1...4p. 107
8.10 Interdependencies Between Languages of Different Levelsp. 107
8.11 The Tree of Sub-structures Dependenciesp. 110
8.12 A General Multi-level Justification Frameworkp. 111
8.13 Design Abstractionsp. 112
8.14 Recommendations for Design and Validation Modelsp. 113
9 Embedded Computer System Structuresp. 117
9.1 States, Events and Other Basic Notionsp. 118
9.2 Notationp. 120
9.3 Level-0. Environment Requirements, Events and Constraintsp. 121
9.3.1 CLM0 Dependability Requirementsp. 121
9.3.2 CLM0 Postulated Initiating Events and Safe Failure Modesp. 122
9.3.3 CLM0 Environment Constraintsp. 122
9.3.4 Level-0 Dependability Case Documentationp. 122
9.4 Level-1. System-Environment Interfacep. 123
9.4.1 Selection of the Entities and Relations of the Interfacep. 123
9.4.2 Environment Statesp. 124
9.4.3 Constraints (NAT)p. 125
9.4.4 A Note on Environment Assumptionsp. 126
9.4.5 Postulated Initiating Events (Relation HAZ[superscript 1])p. 126
9.4.6 System Input-Output Preliminary Specificationsp. 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 Specificationsp. 128
9.4.9 Expansion of the CLM0 Requirements into Primary Claimsp. 129
9.4.10 Primary Validity Claim-Justification Substructuresp. 130
9.4.11 Implementation Primary Claims - Justification Structuresp. 137
9.4.12 Primary Dependability Claims - Justification Substructuresp. 139
9.4.13 Level-1 CLM0 Expansion Structurep. 144
9.4.14 Level-1 Evidence and Delegation Claimsp. 147
9.4.15 Level-1 Argumentp. 149
9.4.16 Level-1 Documentationp. 150
9.5 Level-2. Computer System Architecturep. 151
9.5.1 Elements of the Architecturep. 152
9.5.2 Input and Output Variablesp. 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 Claimsp. 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 Expansionsp. 182
9.5.15 Level-2 Evidence and Delegation Claimsp. 183
9.5.16 A Digression on Testingp. 184
9.5.17 Level-2 Argumentp. 184
9.5.18 Level-2 Documentationp. 185
9.6 Level-3. Designp. 187
9.6.1 Complexity and Elements of the Designp. 187
9.6.2 The Design Relations (SOF[subscript k])p. 187
9.6.3 Design Level Undesired Eventsp. 189
9.6.4 Level-3 Expansion of Level-2 Delegation Claimsp. 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 Expansionsp. 210
9.6.10 Level-3 Evidence and Delegation Claimsp. 211
9.6.11 Level-3 Argumentp. 214
9.6.12 Level-3 Documentationp. 215
9.7 Structure of the Operation Controlp. 216
9.7.1 Elements of the Operation Control Structurep. 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 Claimsp. 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 Expansionp. 234
9.7.9 Level-4 Evidencep. 236
9.7.10 Level-4 Argumentp. 236
9.7.11 Level-4 Dependability Case Documentationp. 237
9.8 Guidance Provided by the System Substructure Treep. 238
9.9 Concluding Remarks: Model Inter-relations and Preservation Propertiesp. 239
Part IV Methodological Implications
10 Pre-existing Systems and Componentsp. 245
10.1 Pre-existing Componentsp. 246
10.2 Composability and Re-use of Argumentsp. 246
10.2.1 Syntactical Conditionsp. 247
10.2.2 Semantic Conditionsp. 247
10.3 Guaranteed Services and Rely Conditionsp. 248
10.4 The System-Component Interface Substructuresp. 250
10.4.1 The GRANT and RELY Relationsp. 250
10.4.2 The HAZ[superscript s] Relationp. 251
10.4.3 Proof Obligations for the Developer of Sp. 252
10.4.4 The U[subscript s]([delta xi subscript s]) Expansion Structuresp. 254
10.4.5 Proof Obligations for the Embedding Systemp. 255
10.4.6 System-Component Interface Revisitedp. 262
10.5 Documentationp. 263
10.6 Concluding Remarks and Justification Issuesp. 265
10.6.1 Completeness of S Specificationsp. 265
10.6.2 Robustness of S Operationp. 267
10.7 Criticality Degrees and Integrity Levelsp. 268
11 Construction Methodsp. 269
11.1 Dependability Case Construction Rulesp. 269
11.1.1 Initial Dependability Requirements Address Product, Not Process Quality Assurancep. 269
11.1.2 A Unique Interpretation Model for the Specification of Initial Dependability Requirements and for the Validation of Preliminary Specificationsp. 270
11.1.3 Expansionsp. 270
11.1.4 Claims Firstp. 271
11.1.5 Expansion and Justification Interpretation Structuresp. 271
11.1.6 Ordering for Claim Elicitation and Justificationp. 272
11.1.7 Primary Claimsp. 273
11.1.8 Level-1 Expansionp. 273
11.1.9 Assumptions Are Not Evidencep. 274
11.1.10 Evidence Must Be Explicitly Claimedp. 274
11.1.11 Claim Identification and Documentationp. 275
11.1.12 Fixed Levels of Expansion and Evidencep. 275
11.1.13 Strict Conjunctionsp. 276
11.1.14 Delegation to the Adjacent Lower Evidence Levelp. 276
11.1.15 Re-use of Argumentsp. 276
11.1.16 Pre-existing Componentsp. 278
11.2 FFP (Functions/Failures/Properties) Methodp. 278
12 Postfacep. 283
A The SIP Systemp. 287
A.1 Descriptionp. 287
A.2 Plant, Technology and Safety Replacement Constraintsp. 289
A.3 Dependability Requirements (CLM0) and Primary Claimsp. 290
A.4 Primary Claims on Software CCF'sp. 291
A.5 Software Architecture and Design. Claims and Evidencep. 292
A.5.1 Operating Systemp. 292
A.5.2 Library Modulesp. 292
A.5.3 Application Softwarep. 293
B Automated Material Handling Systemp. 295
B.1 Descriptionp. 295
B.2 Dependability Requirements (CLM0)p. 296
B.3 Constraints and Postulated Initiating Eventsp. 298
B.4 Preliminary Specifications and Primary Claimsp. 298
Referencesp. 309
Indexp. 317
Go to:Top of Page