ML24115A065
| ML24115A065 | |
| Person / Time | |
|---|---|
| Issue date: | 04/23/2024 |
| From: | Basturescu S, Sushil Birla, Norbert Carte, Mauricio Gutierrez, Derek Halverson NRC/RES/DE |
| To: | |
| Sushil Birla 3014152311 | |
| Shared Package | |
| ML24115A064 | List: |
| References | |
| Download: ML24115A065 (16) | |
Text
Correct-by-Construction Reactor Protection Systems
{Sushil Birla, Norbert Carte, Derek Halverson, Sergiu Basturescu, Mauricio Gutierrez}, U.S. Nuclear Regulatory Commission Workshop on Mathematically Formalized Assurance for National Security (MFANS) Workshop Collaborative Computing Center (C3), 955 MK Simpson Boulevard, Idaho Falls, ID 83415 April 29, 2024 1
Economics!
2 Engineering time Run time Monitor Detect Intervene Diverse redundancy Prevent hazard Prevent propagation Verify Reactive Preventative Cost increases Potential to decrease intrinsic cost 2
2 Introduction to Assured Software Engineering
© 2018 Carnegie Mellon University
[DISTRIBUTION STATEMENT A] Approved for public release and unlimited distribution.
Understanding the Cost of Correcting Defects McConnell, Steve. Software Quality at Top Speed. August 1996.
http://www.stevemcconnell.com/articles/art04.htm 3
Defect-prevention through Refinement Requirements Architecture Detailed design Implementation Abstraction Declarative (what)
Imperative (how)
Concretion R
E F
I N
E M
E N
T 4
4
Leverage domain engineering Development Phase Requirements Architecture Detailed design Implementation Constraints to enable refinement Domain-specific controlled natural language Domain-specific architecture modeling language Domain-specific design specification language Domain-specific coding/programming language Semantically compatible Semantically compatible Semantically compatible refinement refinement refinement Create pre-certified reusable assets Domain modeling Domain engineering (see NUREG/CR-6263; IEEE Std 1517:2010; ISO/IEC 26550) 5 5
Prevention Mitigation Fault tolerance in Design Q
u a
l i
t y
o f
D e
s i
g n
Desired state Current state Changes needed to prevent CCF Objective evaluation criteria Paradigm State of practice Competence Culture 6
6
Reference model Source: ISO/IEC 26550:2015(E) 7
Object is certified Eval Accredited 3rd party Pre-certified Procedures Pre-certified Facilities Pre-certified People Accrediting, certifying authority International common core standards Domain-specific evaluation criteria Rework cycle accredit certify Learning cycle Object of evaluation One vision of the Assurance Process submit derive Evaluation-basis 8
8
Ob Object of pre-certification:
Object is certified Evaluate Accredited certifying authority People Rework cycle Learning cycle Envisioned pre-certification activities Tools Processes Procedures Methods & techniques Facilities Other reusable assets, e.g.:
- Libraries 9
9
Creating the appropriate standards: One vision Ob Technical basis for:
People Tools Processes Procedures Methods & techniques Facilities Other reusable assets, e.g.:
Libraries R&D community Other voices Standards body Standard Guideline develops Government 10 10
Evidence should support consistent judgment Safety claim satisfied unconditionally Residual uncertainty has insignificant effect.
No one can find:
- Any uncontrolled hazard.
- Any unmitigated defeater.
The safety claim is not satisfied with the given evidence.
The evidence gaps are identified.
The safety claim does not hold.
- Fallacies in logic.
- Deficiencies in evidence.
Judge 11 11
Distribution Statement "A: Approved for Public Release, Distribution Unlimited.
If you have any questions, please contact the DARPA Public Release Center (PRC) 12 CLARISSA TOOLS Assurance Case to Logic Program Step 1 ASCE s(CASP
)
Semantic Reasoning Step 2 Human Explainable Logically-Reasoned Assurance Case using ASCE
- Prolog, s(CASP)
Defeater s
Theories Knowledge Assistanc e Engines
- ErgoAI, LLM Logically Integrated Case, Evidence
& Theories Decision Support System Known vulnerabilities Structural &
Syntactic Analysis Semantic Analysis Assurance Case Logic Program (Prolog)
Reasoning Analysis Synthesis Safety Assurance Case: evidence-based reasoning-supported judgment Source: CLARISSA team presentation at ARCOS meeting, Niskayuna NY March 12, 2024
Distribution Statement "A: Approved for Public Release, Distribution Unlimited.
If you have any questions, please contact the DARPA Public Release Center (PRC) 13 ASSURANCE CASE SYNTHESIS Synthesis Assistant is a research tool designed to synthesize claims, arguments and evidence structures from a root or top-level claim.
Given:
Top-level claim (defined in ErgoAI or node imported from an ASCE file)
Definition of the system structure Possible defeaters Theories used to develop the case Evidences for the case NL Claim
- Theories, Evidence Clarissa ASCE Formalised (HiLog)
Synthesised (HiLog)
Graphical and textual summary Synthesis Assistant Selection and integration Clarissa ASCE Source: CLARISSA team presentation at ARCOS meeting, Niskayuna NY March 12, 2024
Discussion
Some opportunities for synergy 1.
Identification & prevention of hazards rooted in engineering 2.
Formulation of safety requirements 3.
Flow-down of requirements specifications 4.
Composability 5.
CPS ontological framework: general; domain-specific 6.
Competence-building Can Education Technology help?
Explore common interest in mathematically-formalized assurance Assurance Case Requirements; Arch design; Detailed design; Implementation Hazard Analysis (e.g. STPA)
Evidence Generation Evidence Integration Formalization of RAAML Semantic gaps SysML AADL Eliminating semantic loss; Minimizing effort; Eliminating data re-entry