Justifying the Dependability of Computer-based Systems (eBook)

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.

Preface 8
Acknowledgements 10
Contents 12
PART I The Context 18
1 Introduction 19
2 Current Practices 24
3 Axiomatic Justification and Uncertainty 27
4 Justification and Dependability Case 31
4.1 Cost Minimization and the Proportionality Principle 32
4.2 Risk-based Assessment 33
4.3 Two Illustrative Case Studies: A Process Instrumentation (SIP) and a Radioactive Materials Handling System 33
PART II Prescriptions 35
5 Requirements, Claims and Evidence 36
5.1 Where to Start? The First Foundation of Dependability Justification 36
5.2 The Initial Dependability Requirements (CLM0) 37
5.3 The Other Foundation: The System Input-Output Preliminary Requirements 41
5.4 Primary Claims 42
5.5 Differences Between Dependability Requirements and Claims 43
5.6 Evidence and Model Assumptions. 45
5.7 How to Organize Evidence? A Four-level Structure 46
5.8 How Are the Four Levels Related? Levels of Causality 49
5.9 Examples 52
6 Arguments, Syntax and Semantics 54
6.1 Claim Assertions 54
6.2 White, Grey and Black Claims 55
6.3 The Inductive Justification Process 56
6.4 The Conjunctive Property 59
6.5 The Syntax of an Argument 62
6.6 Claim and Argument Semantic Aspects 65
7 Axiomatic Principles and Limits 71
7.1 Claim Justifiability 71
7.2 Evidence Plausibility and Weight 73
7.3 The Ineluctability of Consensus 74
7.4 Epistemic Versus Stochastic Uncertainty 76
7.5 Claims on Product Versus Evidence from Process 79
7.6 Logics of Prevention, Precaution and Enlightened Catastrophism 80
7.7 Concluding Remarks on Claims, Arguments, Evidence 81
PART III Descriptions 83
8 Structures and Interpretations 84
8.1 The Roles of Models in Dependability Assessment 85
8.2 Basic Model Notions 86
8.3 On Descriptions and Interpretations 90
8.4 Mathematical Structures 92
8.5 System Structures 93
8.6 L-Interpretations 95
8.7 The Formal Definition of a Model 96
8.8 Validation and Satisfiability Obligations 97
8.9 Interdependencies Between Structures of Different Levels 111
8.10 Interdependencies Between Languages of Different Levels 118
8.11 The Tree of Sub-structures Dependencies 121
8.12 A General Multi-level Justification Framework 122
8.13 Design Abstractions 123
8.14 Recommendations for Design and Validation Models 124
9 Embedded Computer System Structures 127
9.1 States, Events and Other Basic Notions 128
9.2 Notation 130
9.3 Level -0. Environment Requirements, Events and Constraints 131
9.4 Level -1. System-Environment Interface 133
9.5 Level-2. Computer System Architecture 161
9.6 Level-3. Design 197
9.7 Structure of the Operation Control 226
9.8 Guidance Provided by the System Substructure Tree 248
9.9 Concluding Remarks: Model Inter-relations and Preservation Properties 249
PART IV Methodological Implications 253
10 Pre-existing Systems and Components 254
10.1 Pre-existing Components 255
10.2 Composability and Re-use of Arguments 255
10.3 Guaranteed Services and Rely Conditions 257
10.4 The System-Component Interface Substructures 259
10.5 Documentation 272
10.6 Concluding Remarks and Justification Issues 274
10.7 Criticality Degrees and Integrity Levels 277
11 Construction Methods 278
11.1 Dependability Case Construction Rules 278
11.2 FFP (Functions/Failures/Properties) Method 287
12 Postface 292
Appendix A The SIP System 296
A.1 Description 296
A.2 Plant, Technology and Safety Replacement Constraints 298
A.3 Dependability Requirements (CLM0) and Primary Claims 299
A.4 Primary Claims on Software CCF’s 300
A.5 Software Architecture and Design. Claims and Evidence 301
Appendix B Automated Material Handling System 304
B.1. Description 304
B.2 Dependability Requirements (CLM0) 305
B.3 Constraints and Postulated Initiating Events 307
B.4 Preliminary Specifications and Primary Claims 307
References 317
Index 324