| The Context | |
| Introduction | p. 3 |
| Current Practices | p. 9 |
| Axiomatic Justification and Uncertainty | p. 13 |
| Justification and Dependability Case | p. 17 |
| Cost Minimization and the Proportionality Principle | p. 18 |
| Risk-based Assessment | p. 19 |
| Two Illustrative Case Studies: A Process Instrumentation (SIP) and a Radioactive Materials Handling System | p. 19 |
| Prescriptions | |
| Requirements, Claims and Evidence | p. 23 |
| Where to Start? The First Foundation of Dependability Justification | p. 23 |
| The Initial Dependability Requirements (CLM0) | p. 24 |
| PIE's, Constraints, Safe States | p. 25 |
| Elicitation | p. 26 |
| Completeness | p. 27 |
| The Other Foundation: The System Input-Output Preliminary Requirements | p. 28 |
| Primary Claims | p. 29 |
| Differences Between Dependability Requirements and Claims | p. 30 |
| Evidence and Model Assumptions | p. 32 |
| How to Organize Evidence? A Four-level Structure | p. 33 |
| How Are the Four Levels Related? Levels of Causality | p. 36 |
| Examples | p. 39 |
| Arguments, Syntax and Semantics | p. 41 |
| Claim Assertions | p. 41 |
| White, Grey and Black Claims | p. 42 |
| The Inductive Justification Process | p. 43 |
| The Conjunctive Property | p. 46 |
| The Syntax of an Argument | p. 49 |
| Delegations and Expansions | p. 49 |
| Claim Justifications | p. 50 |
| Argument Unicity and Termination | p. 51 |
| Claim and Argument Semantic Aspects | p. 52 |
| Delegation and Expansion as Tools for Refinement of Evidence and Argument Incremental Construction | p. 52 |
| Universal and Existential Claim Assertions | p. 54 |
| Claim Refutation | p. 56 |
| Absence of Level-1 Grey Primary Claims | p. 56 |
| Adjacent Delegation Sub-claims | p. 56 |
| Axiomatic Principles and Limits | p. 59 |
| Claim Justifiability | p. 59 |
| Evidence Plausibility and Weight | p. 61 |
| The Ineluctability of Consensus | p. 62 |
| Epistemic Versus Stochastic Uncertainty | p. 64 |
| Claims on Product Versus Evidence from Process | p. 67 |
| Logics of Prevention, Precaution and Enlightened Catastrophism | p. 68 |
| Concluding Remarks on Claims, Arguments, Evidence | p. 69 |
| Descriptions | |
| Structures and Interpretations | p. 73 |
| The Roles of Models in Dependability Assessment | p. 74 |
| Basic Model Notions | p. 75 |
| Model Structures and Relations | p. 76 |
| Predicates | p. 78 |
| Languages and Proofs | p. 79 |
| On Descriptions and Interpretations | p. 79 |
| Mathematical Structures | p. 81 |
| System Structures | p. 82 |
| L-Interpretations | p. 84 |
| The Formal Definition of a Model | p. 85 |
| Validation and Satisfiability Obligations | p. 86 |
| Language Expansion/Reduction | p. 86 |
| Substructures and Extensions | p. 87 |
| L[subscript 1]-Interpretation (Environment-System Interface) | p. 90 |
| L[subscript i]-Interpretations (i = 2, 3, 4) | p. 96 |
| Interdependencies Between Structures of Different Levels | p. 100 |
| Properties of Justification Structures | p. 100 |
| Properties of Expansion Structures | p. 104 |
| Internal Compound Structure and Interfaces of a Level-i, i = 1...4 | p. 107 |
| Interdependencies Between Languages of Different Levels | p. 107 |
| The Tree of Sub-structures Dependencies | p. 110 |
| A General Multi-level Justification Framework | p. 111 |
| Design Abstractions | p. 112 |
| Recommendations for Design and Validation Models | p. 113 |
| Embedded Computer System Structures | p. 117 |
| States, Events and Other Basic Notions | p. 118 |
| Notation | p. 120 |
| Level-0. Environment Requirements, Events and Constraints | p. 121 |
| CLM0 Dependability Requirements | p. 121 |
| CLM0 Postulated Initiating Events and Safe Failure Modes | p. 122 |
| CLM0 Environment Constraints | p. 122 |
| Level-0 Dependability Case Documentation | p. 122 |
| Level-1. System-Environment Interface | p. 123 |
| Selection of the Entities and Relations of the Interface | p. 123 |
| Environment States | p. 124 |
| Constraints (NAT) | p. 125 |
| A Note on Environment Assumptions | p. 126 |
| Postulated Initiating Events (Relation HAZ[superscript 1]) | p. 126 |
| System Input-Output Preliminary Specifications | p. 127 |
| The System and the Functional Relation (REQ) | p. 128 |
| The Need for a Unique Interpretation for Requirements and System Specifications | p. 128 |
| Expansion of the CLM0 Requirements into Primary Claims | p. 129 |
| Primary Validity Claim-Justification Substructures | p. 130 |
| Implementation Primary Claims - Justification Structures | p. 137 |
| Primary Dependability Claims - Justification Substructures | p. 139 |
| Level-1 CLM0 Expansion Structure | p. 144 |
| Level-1 Evidence and Delegation Claims | p. 147 |
| Level-1 Argument | p. 149 |
| Level-1 Documentation | p. 150 |
| Level-2. Computer System Architecture | p. 151 |
| Elements of the Architecture | p. 152 |
| Input and Output Variables | p. 152 |
| Channel k Data Acquisition (Relations IN[subscript k]) | p. 153 |
| Channel Assignment Relation (IN) | p. 154 |
| Channel k Output Device (Relations OUT[subscript k]) | p. 154 |
| Voting Relations (OUT) | p. 155 |
| Channel k Requirements (REQ[subscript k]) | p. 155 |
| Level-2 Undesired Events (HAZ[superscript 2]) | p. 156 |
| Level-2 Expansion of Level-1 Delegation Claims | p. 158 |
| Expansion of REQ Acceptable Implementation Delegation Claim[1,2] | p. 158 |
| Expansion of REQ Fail-Safe Implementation Delegation Claim[1,2] | p. 164 |
| Expansion of Functional Diversity Delegation Claim[1,2] | p. 169 |
| Expansion of Reliability and Safety Delegation Claims[1,2] | p. 175 |
| Level-2 Expansions | p. 182 |
| Level-2 Evidence and Delegation Claims | p. 183 |
| A Digression on Testing | p. 184 |
| Level-2 Argument | p. 184 |
| Level-2 Documentation | p. 185 |
| Level-3. Design | p. 187 |
| Complexity and Elements of the Design | p. 187 |
| The Design Relations (SOF[subscript k]) | p. 187 |
| Design Level Undesired Events | p. 189 |
| Level-3 Expansion of Level-2 Delegation Claims | p. 191 |
| Expansion of Channel Acceptable Implementation Delegation Claim[2,3] | p. 191 |
| Expansion of Channel Fail-Safe Implementation Claim[2,3] | p. 196 |
| Expansion of Channel Independency Delegation Claim[2,3] | p. 199 |
| Expansion of Reliability and Safety Delegation Claims[2,3] | p. 206 |
| Level-3 Expansions | p. 210 |
| Level-3 Evidence and Delegation Claims | p. 211 |
| Level-3 Argument | p. 214 |
| Level-3 Documentation | p. 215 |
| Structure of the Operation Control | p. 216 |
| Elements of the Operation Control Structure | p. 218 |
| Operation Control Relations READ[subscript k] and ORDER[subscript k] | p. 219 |
| Control of Operation. Undesired Events (HAZ[superscript 4]) | p. 219 |
| Level-4 Expansion of Level-3 Delegation Claims | p. 220 |
| Expansion of Accuracy Delegation Claim[2,4] | p. 220 |
| Expansion of Channel Fail-safe Control Delegation Claim[3,4] | p. 224 |
| Expansion of Channel Reliability and Safety Delegation Claims[2,4] | p. 229 |
| Level-4 Expansion | p. 234 |
| Level-4 Evidence | p. 236 |
| Level-4 Argument | p. 236 |
| Level-4 Dependability Case Documentation | p. 237 |
| Guidance Provided by the System Substructure Tree | p. 238 |
| Concluding Remarks: Model Inter-relations and Preservation Properties | p. 239 |
| Methodological Implications | |
| Pre-existing Systems and Components | p. 245 |
| Pre-existing Components | p. 246 |
| Composability and Re-use of Arguments | p. 246 |
| Syntactical Conditions | p. 247 |
| Semantic Conditions | p. 247 |
| Guaranteed Services and Rely Conditions | p. 248 |
| The System-Component Interface Substructures | p. 250 |
| The GRANT and RELY Relations | p. 250 |
| The HAZ[superscript s] Relation | p. 251 |
| Proof Obligations for the Developer of S | p. 252 |
| The U[subscript s]([delta xi subscript s]) Expansion Structures | p. 254 |
| Proof Obligations for the Embedding System | p. 255 |
| System-Component Interface Revisited | p. 262 |
| Documentation | p. 263 |
| Concluding Remarks and Justification Issues | p. 265 |
| Completeness of S Specifications | p. 265 |
| Robustness of S Operation | p. 267 |
| Criticality Degrees and Integrity Levels | p. 268 |
| Construction Methods | p. 269 |
| Dependability Case Construction Rules | p. 269 |
| Initial Dependability Requirements Address Product, Not Process Quality Assurance | p. 269 |
| A Unique Interpretation Model for the Specification of Initial Dependability Requirements and for the Validation of Preliminary Specifications | p. 270 |
| Expansions | p. 270 |
| Claims First | p. 271 |
| Expansion and Justification Interpretation Structures | p. 271 |
| Ordering for Claim Elicitation and Justification | p. 272 |
| Primary Claims | p. 273 |
| Level-1 Expansion | p. 273 |
| Assumptions Are Not Evidence | p. 274 |
| Evidence Must Be Explicitly Claimed | p. 274 |
| Claim Identification and Documentation | p. 275 |
| Fixed Levels of Expansion and Evidence | p. 275 |
| Strict Conjunctions | p. 276 |
| Delegation to the Adjacent Lower Evidence Level | p. 276 |
| Re-use of Arguments | p. 276 |
| Pre-existing Components | p. 278 |
| FFP (Functions/Failures/Properties) Method | p. 278 |
| Postface | p. 283 |
| The SIP System | p. 287 |
| Description | p. 287 |
| Plant, Technology and Safety Replacement Constraints | p. 289 |
| Dependability Requirements (CLM0) and Primary Claims | p. 290 |
| Primary Claims on Software CCF's | p. 291 |
| Software Architecture and Design. Claims and Evidence | p. 292 |
| Operating System | p. 292 |
| Library Modules | p. 292 |
| Application Software | p. 293 |
| Automated Material Handling System | p. 295 |
| Description | p. 295 |
| Dependability Requirements (CLM0) | p. 296 |
| Constraints and Postulated Initiating Events | p. 298 |
| Preliminary Specifications and Primary Claims | p. 298 |
| References | p. 309 |
| Index | p. 317 |
| Table of Contents provided by Ingram. All Rights Reserved. |