ML23086A001
| ML23086A001 | |
| Person / Time | |
|---|---|
| Issue date: | 03/27/2023 |
| From: | Sushil Birla NRC/RES/DE |
| To: | |
| Sushil Birla 301-415-2311 | |
| References | |
| Download: ML23086A001 (10) | |
Text
State of the Art for Addressing Hazards from Common Causes in Engineering Digital Instrumentation & Control (I&C) Systems Sushil Birla U.S. Nuclear Regulatory Commission, Washington, DC
[leave space for DOI, which will be inserted by ANS]
ABSTRACT In the traditional approach to assure the safety of systems of the highest criticality (e.g., reactor protection systems),
diversity in design has been used to compensate for the unknown unknowns (residual uncertainties). To obtain a comparable level of assurance without diversity in design, the residual uncertainties would have to be much lower.
This motivated an assessment of the state-of-the-art for addressing hazards from common causes rooted in engineering deficiencies. The assessment is based on literature survey and interviews with, and review feedback from, experts in safety-critical digital systems used in other industries, such as avionics, space exploration, automotive, and medical devices. The state-of-the-art included technological capabilities which have been demonstrated in leading-edge implementations, but their usage may not have been scaled up. The investigation searched the technical literature to find different categories of hazard-contributing engineering deficiencies which could be discovered at each phase of development in a commonly used reference model. Then, for each category, the study identified the conditions to prevent those deficiencies, and the methods for satisfying the preventative conditions. Next, the study identified an approach to integrate all the diverse evidence to reach a consistent conclusion and approaches to reduce inconsistencies in judgment about the residual uncertainty. The findings indicate that the state-of-the-art can support consistent judgment based on objective, scientific evidence and logical reasoning.
Keywords: Digital Instrumentation & Controls; Software Systems Safety Engineering; Safety assurance; Embedded and cyber-physical systems.
- 1. INTRODUCTION The NRC surveyed the state-of-the-art for addressing hazards contributed through engineering deficiencies which could compromise redundancy across independent divisions, defense in depth, or other means of fault tolerance provided for such critical functions as reactor protection in a nuclear power plant (NPP) such compromises are popularly known as common cause failure. In this context the state-of-the-art included technological capabilities which have been demonstrated in leading-edge implementations, but their usage had not been scaled up. The purpose was to assess whether a performance-based (safety outcome focused) approach was technically feasible to achieve a level of assurance obtained in current practice through the provision of diversity in design or such other prescriptions. The study included a combination of literature survey and review feedback and discussions with subject matter experts in non-nuclear application domains (e.g.: aviation; space exploration; automobiles; medical devices). 1 1
The views expressed herein are those of the author and do not represent an official position of the U.S. NRC.
- 2. COMMON CAUSES OF HAZARDS AND THEIR PREVENTION As hazard identification has been well-known to be one of the weakest links in the chain, the study started with a search for the best methods available and the well-known pitfalls in hazard identification (Section 2.1). Then, building on prior NRC research [1], the study searched for different categories of hazard-contributing engineering deficiencies which could be discovered at each phase of the development process, e.g.: specification of requirements (Section 2.2); architecture specification (Section 2.3); detailed design (Section 2.4); unit implementation and verification (Section 2.5). For each category, the study identified the conditions to prevent those deficiencies, and the methods for satisfying the preventative conditions. As the state-of-the-art methods leveraged tool-assisted automation in all development phases, the study also included tool qualification (Section 2.6). As performance-based approaches allow the flexibility of achieving assurance in many ways, the study identified approaches for integrating all the diverse kinds of evidence to reach a consistent conclusion (Section 3.1) and approaches to reduce inconsistencies in judgment about the residual uncertainty (Section 3.2). The findings indicate that the state-of-the-art can support consistent judgment based on objective, scientific evidence and logical reasoning.
Figure 1. Safety analysis (including hazard analysis [HA]) in relation to development phases and verification.
2.1. Hazard Identification: Addressing Common Weaknesses Identifying what can go wrong (i.e., hazard identification) is the most difficult and elusive element of the risk triplet (what can go wrong; what are the consequences; what is the likelihood?) used in the NRCs risk analysis. Thus, in hazard analysis, which consists of hazard identification and hazard control, the former is more challenging. In this study, hazard identification culminates with the specification of the safety constraints to control the hazard. In a safety-focused performance-oriented paradigm, safety requirements, including constraints, are primarily a result of a hazard identification. Hazard control includes the subsequent engineering to satisfy those safety constraints. Referring to the reference model depicted in Figure 1, as part of safety analysis (left column), hazard analysis (blocks labeled HAp, HAc, HAr, HAa, HAdd, HAi, ) is performed at every phase, independent of the development (middle column) and verification (Vc, Vr, Va in the right column). The study identified 16 categories of causes leading to deficiencies in hazard identification. An example is given next:
Identifier HI-9: Hazards in modes of operation/usage other than the at power normal mode, or in transition from one mode to another, are not adequately understood.
Conditions to address HI-9: Hazard analysis is performed for all modes of usage and mode transitions, identifying corresponding safety constraints.
The study identified 3 major factors (mentioned in their approximate order of influence) affecting the quality of hazard identification: (1) Competence of the performers, (2) Quality of the input information, and (3) Method.
Competence: The requisite competence is not easily available in a single individual and requires teamwork, because it includes many dimensions: Mastery of the engineering disciplines, technologies, products or components, processes, and dependencies involved in each phase of the system-development lifecycle; Learnings from operating experience about what can go wrong; Knowledge of the environment of the safety system and its development; Ability to assimilate knowledge and information in a scientifically sound framework; Reasoning capability; Communication skills; Other interpersonal skills.
Input quality: Typically, the input information is in the form of textual narratives and block diagrams, but much is left implicit, i.e., its quality is far from ideal. The analyst must spend considerable effort with probing enquiries or fill in the implicit information with personal experience.
Method: The study identified 16 methods of hazard identification. For identifying systematic causes, System-Theoretic Process Analysis (STPA) [2] has been applied to modern safety-critical digital systems in many application sectors and shows the most promise. Hazard and Operability Studies (HAZOPS) [3][4] has been used in the chemical process industries for a much longer time. Its key success factors include: An experienced facilitator (i.e., HAZOPS process guide); Teamwork; Systematizing inquiry through keywords; Systematizing understanding effects through understanding the associated deviations. These success factors can be used in other methods also.
2.2. Requirements Specification: Addressing Common Deficiencies Referring to Figure 1, the NPP-level hazard analysis produces the initial requirements for a (digital) safety system. As the system development progresses, requirements from the NPP level are refined with additional safety constraints identified through hazard analysis (HAr, HAa, ). Even after identifying a primary hazard at the top-level system, additional hazardous conditions could arise from deficiencies in formulating the safety requirements and constraints to control the identified hazards. Furthermore, deficiencies in the flow-down (decomposition, derivation, and allocation) of these requirements could lead to additional hazardous conditions. Requirements flow down the integration hierarchy, i.e., from system to subsystem to component to subcomponent. Hazard-contributing conditions could occur in each
level of integration. Requirements also flow down the development phase products architectural specification serves as the set of constraints for the detailed design, which, in turn, serves as the set of constraints for the implementation (e.g., coding). The flow is not unidirectional. For example, the hazard analysis of an architectural specification might lead to a change in some requirement specification, which might lead to a change in the architectural specification. This cycle may repeat until no hazard remains uncontrolled. Thus, the categories are not mutually exclusive. The deficiencies in an earlier phase can also be found in later phases. The study identified 60 categories of causes of deficiencies in requirements specification and corresponding conditions to address those deficiencies. Following is an example of a deficiency in requirements:
Identifier RS-22: Interrelationships and interdependence across requirements are not clearly understood or recognized, resulting in unanalyzed conditions.
Conditions to address RS-22: Interrelationships and interdependence across requirements are explicit and under configuration control. There are no hidden dependencies across functions.
Methods to improve safety constraints: While hazard analysis is the primary source of identifying safety constraints, as seen in the example above, initially these constraints or conditions describe the intent in informal natural language and may entail ambiguities. Therefore, they must be transformed into specifications suitable for engineering the system. This transformation and its validation are primarily a cognitive activity, dependent on a broad range of human expertise. Correspondingly, review, walkthrough, and inspection (RWI) are the key method of validation. The informal description is transformed into a restricted natural language [5]. For specifying behavior of systems of interest in this context, the finite state machine paradigm is well suited; the SCR (software cost reduction) method is a requirements specification method based on this paradigm [6]. Modeling languages and environments, originally oriented to architecture description, have been extended to support requirements specification. This approach to modeling requirements (i.e., creation of a domain model) is recommended in [7]. These methods intrinsically support improved validation and verification (V&V) of requirements specifications by enabling the use of math-based methods such as theorem proving and model-checking [8].
2.3. Architecture Specification: Addressing Common Deficiencies Architectural deficiencies can be found at every level of integration. The combination of deficiencies in requirements and architectural specifications contribute most of the hazardous conditions. Following is an example of an architectural deficiency:
Identifier AS-5: Dependencies through resource sharing are not recognized and analyzed for hazards.
Conditions to address AS-5: Unintended interactions between a system, device or other element (internal or external to a safety system) that cause adverse effects on a safety function are avoided. Freedom from interference (including fault propagation) is assured provably across shared resources.
Methods: These conditions can be satisfied with model-based and math-based methods (e.g.: theorem proving; model checking) and their automation [9]. Other modeling environments are also available
[10][11][12]. Transformations of Requirements to Architecture to Detailed Design to Implementation are progressive abstraction-concretion relationships. Refinement (explained in Appendix D of [1]) is a method in which the work product of the next phase satisfies its specification (output of the preceding phase) and does not add any unspecified behavior visible at its external interface. Thus, the work product is correct by construction.
2.4. Detailed Design: Addressing Common Deficiencies A detailed design specification constrains the architecture internal to a component identified in the architecture discussed in Section 2.3. It is the specification to be satisfied by the implementation (e.g.,
code or firmware). Most of the causes of deficiencies identified in the Section 2.3 apply to the intra-
component architecture also. Detailed design includes the specification of control flow, data flow, and data structures to prevent unnecessary coupling and thus, prevent and contain faults and avoid unsafe or hard-to-verify conditions. The study identified 11 categories of causes resulting in deficiencies in detailed design specifications. Following is an example:
Identifier DS-1: Loss of information across disciplines.
Conditions to address DS-1: Methods and languages to describe, represent, or specify the intra-component architecture support unambiguous transformations or mappings across dissimilar (e.g.,
hardware and software) elements. The respective languages are constrained accordingly.
Methods: The methods mentioned earlier are also applicable for improving detailed design. The state of the art in the timing analysis is presented in Appendix I of [1]. A timing analysis is useful in developing and validating timing constraints and validating that the design satisfies these constraints.
2.5. Unit Implementation & Verification: Addressing Common Deficiencies In this context, unit implementation is the transformation of a detailed design into a software component or a logic library block, ready for integration with other components of a system. The study identified 9 cause categories resulting in unit implementation deficiencies and 5 cause categories resulting in unit verification deficiencies. The study excluded deficiencies encountered during integration and integrated verification because these are rooted in upstream deficiencies.
Following are a couple of examples showing unit implementation and verification deficiencies and conditions to prevent them:
Identifier I-4: Timing problems prevent deterministic behavior and are difficult to diagnose and resolve.
Conditions to address I-4: Behavior is not degraded due to execution timing: (1) The results produced by the programmed logic do not depend on either the time taken to execute the program or the time (referring to an independent clock) at which execution of the program is initiated; (2) Execution speed does not affect correct order of execution.
Identifier I-5: Behavior is not analyzable mathematically or analysis is not mechanizable due to the improper use of interrupts or other mechanisms affecting the order of execution.
Conditions to address I-5: Flow-down, refinement, and elaboration of timing constraints (e.g., constraints on concurrent physical processes, inter-process synchronization, and shared resources) is correct (as determined through mathematical analysis). Following are a couples of examples showing unit verification deficiencies and conditions to prevent them:
Identifier V-1: Heavy reliance on testing at the end of the product development cycle.
Conditions to address V-1: The best available preventative methods are used in upstream phases.
Recognizing that even after applying the right combination of best practices and state-of-the-art approaches, some uncertainties may remain in the preventative approaches and the resulting specifications at each phase, the effects of these uncertainties are considered in designing unit verification. Best practices in unit verification include a combination of the following:
- 1. Correct-by-construction methods.
a) The model of the detailed design, including the algorithm, is automatically transformed into a programming language (source code) using a certified configuration of a certified tool; the source code is transformed into executable code, using a certified configuration of a certified compiler.
b) At each transformation, pre-certified libraries are integrated into the code.
- 2. Safe subset of the programming language:
a) Constraints and configuration settings in the programming tools allow only a safe subset of the programming language and a safe subset of the functionality provided by the tools.
b) Whether code creation is mainly manual, automation-assisted, or autogenerated, the tool checks that only safe constructs are used.
- 3. Interface type matching: Tools assist in checking for mismatches between interacting subcomponents, e.g., inputs received are not of the type expected.
- 4. Strongly typed programming language is used.
- 5. RWI methods are used primarily for resolving anomalies.
- 6. Hazard analysis of the source code is used for critical code, e.g., as a specialized part of RWI.
- 7. Static analysis of the source code.
- 8. Model checking.
- 9. Testing, focused on residual uncertainties in preceding development phases and hazard-contributing conditions. With the support of automation, near-exhaustive coverage is feasible through combinatorial testing [13]. It is feasible to cover the explicitly specified operating profile, in conjunction with input validation.
It is technically feasible to verify a unit of logic within a system such as one for reactor protection. This has been demonstrated in much larger systems, including a compiler [14] and an operating system kernel
[15].
2.6. Tool Qualification Although proper use of tool-enabled automation can remove most sources of uncertainties encountered in current practice, tools (and the associated languages) can introduce new kinds of uncertainties. This study identified conditions to reduce these uncertainties; following are some examples. The development environment is qualified and certified for the domain of usage. The integrated development environment (including libraries and such other reusable assets) is validated (independently of its users) for avoiding introduction of defects in the work product (often achieved by constraining its full functionality to a safe subset). Restrictions for safe use of a tool are identified explicitly and enforced through constraints on the usage of the tool. Configuration of the integrated development environment is controlled, including the set of restrictions for safe use. Semantics are preserved in information exchanged across the tools.
Methods for specifying behavior (e.g., finite state machine models) have consistent semantics across different elements of a system and different phase-wise work products of a particular element.
Unambiguous transformation, mapping, elaboration and integration (including composition of essential properties) is ensured across development phases, different elements of the system, and elements from different suppliers. Automation used for the creation of a work product is independent of automation used for the V&V of that work product. V&V tools are qualified using methods that are independent of the methods used to qualify the development tools. A suite of tools (and associated languages), configured for a specific domain, enable a combination of domain engineering and refinement methods to yield correct-by-construction work products, as demonstrated in a recent NRC research project [16].
The approaches for assurance of the system (which were identified earlier) are also applicable to the qualification of a tool. Thus, as observed in preceding sections, automation can perform most of the repetitive work to check that a tool performs as specified under the specified conditions of use. Still, considerable RWI by specialized experts is needed, e.g., to check for the satisfaction of conditions.
- 3. INTEGRATING THE EVIDENCE AND EVALUATING SYSTEM SAFETY To reach a safety conclusion about the overall system, evidence generated by using the methods reviewed in earlier sections (including the uncertainty associated with each item of evidence) must be integrated and organized in a manner that supports intellectual reasoning to evaluate the effect of the residual uncertainty on the safety function. Section 3.1 surveys the corresponding state-of-the-art. Even with state-of-the-art methods for generating and integrating evidence, judgment is required for which Section 3.2 provides a state-of-the-art approach.
3.1. Reasoning about Residual Uncertainty Organizing Information The concept of proving a case based on evidence has been a part of the judicial system in many societies.
Toulmin [17] had formalized the concept for use in the social sciences in the 1950s; Figure 2 depicts an adaptation of the Toulmin model. The UK regulatory bodies began requiring a safety case before granting a license to operate, starting with the nuclear industry in the 1950s; chemical, in the 1970s; offshore, in the early 1990s; and railway, in the mid-1990s. The Computer Science discipline refined the Toulmin model to support reasoning about software and software-dependent systems. ISO and IEC jointly incorporated this concept in the ISO/IEC standard 15026 [18], calling it an assurance case [19]. In order to facilitate the use of structured assurance cases for producing and reviewing ISO/IEC 15026-2 [19]
conformant assurance cases and the associated information exchange, the structured assurance case metamodel (SACM) was created [20]. Industrial-scale projects have used the assurance case framework, implemented through either the Goal Structured Notation (GSN) [21] or the Claims, Arguments, and Evidence notation [22].
Figure 2. Structure for reasoning about the effect of a hazardous condition on the safety conclusion.
The ISO15026 [18] model has provisions for expressing a claim as a composition of sub-claims. The model also has provisions for expressing uncertainty as a logical condition and associating it with a claim or sub-claim: the conditions or cases not covered in the V&V are associated with the claim or sub-claim as logical expressions; then, compositions carry these conditions up the assembly hierarchy, using prespecified rules. In Figure 2, conditions or cases not covered are depicted as qualifiers associated with the claim or sub-claim. These provisions support understanding the effect of uncertainties on the claim. The compositional relationships can be represented in the architectural model, providing a basis for reasoning about the combined effects of various uncertainties. Thus, the assurance case model can be derived from the architectural model in a mechanized manner using a parameterized set of rules [23]. This capability has been demonstrated using RESOLUTE [24], a language (an annex to AADL [25]) and tool
[26] to create an assurance case, based on an architectural model specified in AADL. A rule specified in RESOLUTE defines the relationship of a claim in the assurance case and the evidence which satisfies the claim. Parameterized claims and rules are reusable assets, accessible through an associated library. Thus,
an assurance case could be composed from such reusable assets. ADVOCATE [27] is another approach to reduce the human effort in the creation of assurance cases.
The state-of-the-art to prove, demonstrate, or evaluate that the residual uncertainty is not significant to the safety conclusion utilizes a combination of the following: Evidence from work products of all development phases; Sound reasoning relating scientific evidence (e.g., results of V&V) to the safety conclusion; Judgment to conclude that the residual uncertainty is not significant to the safety conclusion.
Bloomfield and Rushby have identified an approach to systematize this combination [28], especially ways to reason about the residual uncertainty (i.e., the gaps between scientific evidence-based deductive reasoning and assurance of the claim with certainty). They refer to these gaps as doubts or defeaters, which could be mapped into counterclaims. Then, their process focuses effort on defeating the defeaters, i.e., making the argument indefeasible. They argue that the systematized search for defeaters on the one hand and indefeasibility, on the other helps overcome confirmation bias Section 2.8 broadens the issue to other cognitive biases and broadens the systematization of judgment correspondingly. They frame their approach in the hazard analysis paradigm treating bias as a form of hazard. Figure 2 depicts this kind of reasoning in the form of qualifiers, factors affecting validity, challenges, and rebuttals.
3.2. Improved Expert Judgment to Reason About Residual Uncertainty Even after applying the best practices and state-of-the-art approaches identified in the preceding sections, there may be remaining uncertainties. Reasoning about the effect of these residual uncertainties on the safety function requires human cognitive effort. Human reasoning entails heuristics which tap into implicit knowledge and provide shortcuts in the reasoning pathways but can lead to cognitive biases of many kinds (e.g., confirmation bias, availability heuristic, halo effect, false-consensus effect, anchoring bias, optimism bias, hindsight bias, misinformation effect, actor observer bias, and self-serving bias)
[29][30].
Uncertainty-reduction depends significantly upon the ability to neutralize or overcome the effect of such cognitive biases. Science-based approaches are available to reduce the effects of these cognitive biases one approach is described next. A team of properly selected experts exercises judgment, following a teamwork process conducive to the expression of their individual reasoning approaches and the neutralization of their individual cognitive biases. The team should consist of at least 3 core members 2 to bring diverse viewpoints and one to facilitate the process, maintaining balance between the diverse perspectives. Collectively, the core team should have the breadth of knowledge to understand how various sources of uncertainty influence the overall assurance case. Each member of the core team should be able to assimilate knowledge and information in a scientifically sound framework. The core team may be augmented with issue-specific independent V&V specialists as needed to understand some issue-specific uncertainty for its effect on the safety conclusion. If there are many multidimensional interrelated issues, additional core members may be effective. However, a core team of more than 5 experts may become unmanageable. The facilitator should be skilled in social interaction processes, proficient in evidence-based reasoning, and capable of identifying logical fallacies.
Following is an example of a judgment exercising process. The experts outline their plan of work collectively, with consensus on the uncertainties of concern and the general sequence of their analysis.
The facilitator leads the execution of the plan, adjusting it as needed, drawing out diverse perspectives, and overcoming cognitive biases to the extent feasible. The experts engage in the evaluation early in the development process, starting with a review of the initial safety plan and the supporting V&V plan at the concept phase of system development. The safety plan should include the envisioned structure of the safety assurance case. At the end of each development phase, the developers provide the evidence generated from that phase and update the safety plan and the V&V plan; the expert judgment team reviews the evidence and the updated plans and updates its own work plan accordingly.
Stopping condition: Expert judgment aims to reach a conclusion (Rushby and Bloomfield call it sentencing [28]) as follows:
EITHER: The safety claim is satisfied unconditionally (i.e., the residual uncertainty has an insignificant effect on the safety claim).
OR: The safety claim is not satisfiable with the given evidence the residual uncertainty is so great that the safety claim cannot be supported; the defeaters are identified.
OR: The safety claim does not hold.
- 4. CONCLUSIONS The NRC assessed the state-of-the-art for addressing hazards contributed through engineering deficiencies which could compromise redundancy across independent divisions, defense in depth, or other means of fault tolerance provided for such critical functions as reactor protection such compromises are popularly known as common cause failure. The motivation was to explore whether the state-of-the-art for engineering such systems enabled a level of assurance comparable to the level of assurance achieved in current practice through diversity in design. While the study showed technical feasibility, it also revealed challenges in applying the technology at scale in practice, e.g.: validating results of hazard analysis; validating assumptions about the environment of the system of interest; qualifying a suite of engineering tools from different sources; lack of an infrastructure for independent V&V.
ACKNOWLEDGMENTS NRC colleagues, Mauricio Gutierrez, Bernard Dittman, and Pong Chung managed the project to conduct this study. Several experts outside the NRC provided leads, suggestions, stimulating questions, and review inputs, including Dr. Richard Kuhn, Dr. Paul Black and Dr. Edward Griffor from National Institute of Science and Technology, Dr. Alwyn Goodloe from National Aeronautics and Space Administration, Pascal Regnier and Jean Gassino from Institut de Radioprotection et de Surete Nucleaire (France), and Mark Bowell from Office of Nuclear Regulation (UK); previously, Professors (late) John Knight, Mats Heimdahl, Alan Wassyng, John Stankovic, John McDermid and Manfred Broy had provided inputs to NRC Research Information Letter 1101 [1].
REFERENCES
[1] U.S. Nuclear Regulatory Commission, Research Information Letter 1101: Technical basis to review hazard analysis of digital safety systems, https://www.nrc.gov/docs/ML1321/ML13219A344.pdf (2013).
[2] N. Leveson and J. Thomas, STPA Handbook, https://psas.scripts.mit.edu/home/get_file.php?name=STPA_handbook.pdf (2018).
[3] Chemical Industries Association, Chemical Industry Safety and Health Council (CISHEC), A Guide to Hazard and Operability Studies, London, UK (1977).
[4] International Electrotechnical Commission, Hazard and Operability Studies (HAZOP Studies)
Application Guide, IEC 61882:2001, Edition 1.0, Geneva, Switzerland, (2001).
[5] T. Kuhn, A survey and classification of controlled natural languages, Computational Linguistics, 40 (1) (2014).
[6] C.L. Heitmeyer, et al., Applying a formal requirements method to three NASA systems: lessons learned, IEEE Aerospace Conference, Big Sky, Montana, March 3-10 (2007).
[7] U.S. Nuclear Regulatory Commission, High Integrity Software for Nuclear Power Plants NUREG/CR-6263, Vol 2 (1995).
[8] International Electrotechnical Commission, Functional safety of electrical/electronic/
programmable electronic safety-related systems - Parts 1 to 7, IEC 61508 (2010).
[9] D. Stewart, M.W. Whalen, D. Cofer, and M. P. Heimdahl, Architectural Modeling and Analysis for Safety Engineering, Proceedings of International Symposium on Model-Based Safety and Assessment (IMBSA 2017), Trento, Italy, pp.97-111, September 11-13 (2017).
[10] https://www.ansys.com/products/embedded-software/ansys-scade-suite.
[11] https://essr.esa.int/project/taste.
[12] https://www.nxtcontrol.com/en/engineering/.
[13] https://csrc.nist.gov/projects/automated-combinatorial-testing-for-software.
[14] X. Leroy, Formal certification of a compiler back-end or: programming a compiler with a proof assistant, Proc. 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Charleston, SC, January 11-13, pp. 42-54 (2006).
[15] G. Klein, et al, Comprehensive Formal Verification of an OS Microkernel, ACM Transactions on Computer Systems, Vol. 32 (1), pp. 1-70, (2014).
[16] https://github.com/GaloisInc/HARDENS
[17] S. Toulmin, The Uses of Argument, Cambridge University Press, Cambridge, UK (1958).
[18] IEEE Std 15026-1-2014, Adoption of ISO/IEC 15026-1, Systems and Software Engineering Systems and Software AssurancePart 1: Concepts and vocabulary, (2014).
[19] IEEE Std 15026-2-2011, Adoption of ISO/IEC 15026-2:2011, Systems and Software EngineeringSystems and Software AssurancePart 2: Assurance Case (2011).
[20] https://www.omg.org/spec/SACM/About-SACM/.
[21] https://www.goalstructuringnotation.info/.
[22] https://www.adelard.com/asce/choosing-asce/cae.html.
[23] A. Gacek, et al, Resolute: an assurance case language for architecture models, Proc. ACM SIGADA Conf. on High integrity language technology, Portland, Oregon, Oct 18-21 pp. 19-28, (2014).
[24] https://github.com/loonwerks/Resolute.
[25] https://www.sae.org/standards/content/as5506c/.
[26] http://www.aadl.info/aadl/currentsite/tool/osate.html.
[27] E. Denney, G. Pai, and J. Pohl, AdvoCATE: An assurance case automation toolset, Proceedings of the International Conference on Computer Safety, Reliability, and Security (SAFECOMP),
Magdeburg, Germany, September 25-28, pp. 8-21, (2012).
[28] R. Bloomfield and J. Rushby, Assurance 2.0: A Manifesto, http://www.csl.sri.com/~rushby/papers/assurance2-arxiv.pdf (2021).
[29] A. Tversky and D. Kahneman, Judgment under uncertainty: Heuristics and biases, Science, 185 (4157), pp.1124-1131 (1974).