ACCESS: Assurance Case Centric Engineering of Safety-critical Systems

This paper introduces ACCESS, an engineering methodology and tool suite that enables the development of safety-critical systems through evolving, model-based assurance cases capable of tracing heterogeneous artifacts, integrating formal methods, and supporting automatic evaluation at both development and runtime, as demonstrated by an Autonomous Underwater Vehicle case study.

The Gist

Imagine you are building a very complex, self-driving underwater robot. You want to be 100% sure it won't crash into things or get lost. In the old days, proving it was safe was like writing a giant, static paper report. You'd write down your arguments, paste in some photos of the design, and hope a human inspector would read it all and say, "Looks good." But if you changed one tiny screw in the robot, you'd have to rewrite the whole report and hope you didn't miss a connection.

This paper introduces a new way of doing things called ACCESS. Think of ACCESS not as a paper report, but as a living, breathing digital dashboard that sits in the center of your project.

Here is how it works, broken down into simple concepts:

1. The "Living Report" (The Assurance Case)

Instead of a static document, ACCESS treats the safety argument as a central hub connected to everything else.

• The Old Way: Imagine a map drawn on paper. If the terrain changes, the map is useless until you redraw it by hand.
• The ACCESS Way: Imagine a GPS app. The "safety argument" is the destination, but it's connected to live traffic data, road conditions, and your car's engine status. If the road changes, the app knows instantly.

2. The "Digital Twin" Connection

The paper describes a system where the safety argument is linked directly to the actual engineering models (the blueprints, the code, the safety checks).

• The Analogy: Think of the safety argument as a safety inspector standing next to a robot. In the past, the inspector had to ask, "Did you check the brakes?" and wait for a human to go look.
• With ACCESS: The inspector is connected to the robot's brain via a wire. When the robot's design changes, the inspector's clipboard updates automatically. If the robot's new design has a flaw, the inspector's clipboard immediately flashes red.

3. The "Magic Toolbox" (ACME)

The authors built a software tool called ACME (Assurance Case Management Environment) to make this happen.

• What it does: It acts like a universal translator and a spell-checker rolled into one. It can read different types of files—Excel spreadsheets, complex 3D models, and even mathematical proofs—and link them all to the safety argument.
• The Superpower: It doesn't just store the files; it checks them. If you change a number in an Excel sheet (like the failure rate of a battery), ACME runs a quick calculation to see if the safety argument still holds up. If it doesn't, it tells you exactly where the problem is.

4. The "Self-Driving" Safety Check

The paper also talks about what happens when the robot is actually working underwater (runtime).

• The Concept: Usually, safety checks happen before the robot is built. ACCESS wants to keep checking while it's working.
• The Analogy: Imagine your car has a dashboard light that says "Engine Safe." Usually, that light is just a sticker. In ACCESS, that light is connected to the engine's sensors. If the engine starts acting weird while you are driving, the "Safety Light" turns red immediately, and the car knows to slow down or stop.
• The Result: The safety argument isn't just a document for the past; it's a real-time monitor for the present.

5. The Proof (The AUV Case Study)

To prove this works, the authors tested it on an Autonomous Underwater Vehicle (AUV).

• They built the robot's safety argument using their new method.
• They linked it to the robot's design models and mathematical proofs.
• They showed that when they changed the design, the system automatically flagged errors.
• They even showed how the system could check the robot's sensors while it was "driving" (simulated), ensuring the data it was seeing was still safe.

The Bottom Line

The paper claims that ACCESS makes building safe robots faster and more reliable.

• Faster: Because you don't have to manually rewrite safety reports every time you change a design. The computer does the linking and checking for you.
• More Reliable: Because the safety argument is always connected to the real data. You can't accidentally forget to update a safety rule because the computer won't let the system "pass" if the data doesn't match.

In short, ACCESS turns safety assurance from a static, manual paperwork exercise into a dynamic, automated, and living process that grows and changes right alongside the robot it protects.

Technical Summary

Technical Summary: ACCESS – Assurance Case Centric Engineering of Safety-critical Systems

1. Problem Statement

Safety-critical systems require explicit justification of their safety to operate within defined contexts. Traditionally, Assurance Cases (arguments supported by evidence) are manually created documents evaluated through lengthy, error-prone processes. As systems become more complex and interconnected, managing the development life-cycle, including the coordination of verification, validation, and change impact analysis across heterogeneous engineering artifacts, becomes increasingly difficult.

Furthermore, the emergence of Robotics and Autonomous Systems (RAS) introduces challenges that traditional assurance approaches cannot address. RAS are often open and adaptive, requiring assurance cases that can evolve during the operational life of the system with minimal human intervention. Current methodologies lack sufficient model-based foundations to:

1. Systematically trace assurance cases to diverse engineering artifacts (e.g., architectural models, safety analyses, behavior models).
2. Automate the collective evaluation of assurance cases and their referenced artifacts.
3. Shift safety assurance activities from development time to runtime to handle dynamic environments.
4. Integrate formal methods results directly into the assurance argumentation.

Existing notations like Goal Structuring Notation (GSN) and Claim-Argument-Evidence (CAE) do not natively support the traceability to external artifacts required for automated, coherent assurance.

2. Methodology: ACCESS

The paper proposes ACCESS (Assurance Case Centric Engineering of Safety-critical Systems), an engineering methodology that develops safety-critical systems around an evolving, model-based assurance case. ACCESS adopts principles of Model-Based Systems Engineering (MBSE), treating models as first-class artifacts.

The methodology consists of seven iterative steps, coordinating System Development and System Assurance activities:

• Step 1: Plan Assurance Case: Define system functions, hardware platforms, and environmental assumptions. Perform high-level safety analysis (e.g., HARA) to derive preliminary safety goals.
• Step 2: Create Assurance Case: Model the system architecture and specify modular assurance case modules. Generate public claims for allocated requirements and define assumptions for peer subsystems.
• Step 3: Refine Assurance Case: Perform subsystem safety analyses (e.g., FMEDA) and allocate requirements to subsystems. Develop safety arguments for each subsystem, maintaining traceability to requirements.
• Step 4: Validate and Verify Engineering Artifacts: Create behavioral models (e.g., state machines) with formal semantics. Perform model analysis and verification to ensure requirements are satisfied and model integrity (e.g., deadlock freedom) is maintained.
• Step 5: Evaluate Assurance Case: Implement the system and perform system-level verification and validation. The assurance case is evaluated collectively, with unsupported claims triggering re-evaluation of previous steps.
• Step 6: Convert to Dynamic Assurance Case: For RAS, convert specific parts of the assurance case to "dynamic" forms. This involves defining runtime data drivers that link operational data to engineering models, allowing the assurance case to reflect the system's current state.
• Step 7: Automated Runtime Evaluation: Perform non-invasive, automated periodic evaluations of the dynamic assurance case using runtime data. If validity is lost, the system can transition to a safe state.

3. Tool Support: ACME

To support ACCESS, the authors developed the Assurance Case Management Environment (ACME). ACME is a model-based framework built on the Eclipse Modelling Framework (EMF) and the Structured Assurance Case Metamodel (SACM).

Key capabilities of ACME include:

• Traceability: Fine-grained tracing from assurance case elements (Goals, Solutions, Contexts) to heterogeneous engineering artifacts (EMF models, Excel spreadsheets, Isabelle theory files).
• Automated Validation: Execution of model queries (using Epsilon Object Language - EOL) to validate engineering artifacts against assurance case constraints.
• Formal Integration: Connection to an Isabelle/HOL server to verify formal theories (e.g., deadlock freedom proofs) and generate Isabelle/SACM representations of the assurance case for logical integrity checking.
• Dynamic Assurance: Support for Runtime Data Drivers and a Dynamic Safety Management System (DSMS) to synchronize runtime data with assurance models and perform continuous evaluation.

4. Case Study and Results

The methodology and tooling were applied to a case study involving an Autonomous Underwater Vehicle (AUV). The AUV's safety controller (Last Response Engine - LRE) was modeled using RoboChart (a graphical language with formal CSP semantics).

Key Findings from the Case Study:

• Traceability: The team successfully traced safety arguments to FMEDA results in Excel spreadsheets, RoboChart behavioral models, and Isabelle formal proofs.
• Automation: ACME automatically executed validation rules on the Excel FMEDA data and invoked the Isabelle server to check formal proofs. Errors in models (e.g., missing transitions or failed proofs) were immediately flagged in the assurance case editor.
• Runtime Adaptation: The LRE assurance case was converted to a dynamic form. Runtime sensor data (obstacle readings) were synchronized to the model, and validation rules checked if sensor readings remained within safe bounds.
• Efficiency Evaluation: Comparative experiments were conducted on a power supply unit (System A) and a navigation unit (System B) using three approaches:
  1. Manual (Text-based).
  2. Model-based without ACME.
  3. Model-based with ACME.
  • Results: The manual approach took significantly longer (e.g., 505 minutes for System A) and could not support runtime assurance. The model-based approach without ACME reduced time (262 minutes). The approach with ACME support was the most efficient (~87 minutes for System A), demonstrating a substantial reduction in development effort.
• Scalability: ACME successfully handled models with up to ~5,689 elements. However, scalability tests indicated memory overflow issues when model element counts reached the millions, attributed to the need to load entire EMF models into memory for querying.

5. Significance and Contributions

The paper claims the following main contributions:

1. ACCESS Methodology: A critical systems engineering methodology centered on an evolving assurance case model, bridging the gap between development and runtime assurance.
2. Automated Evaluation: A framework for evaluating assurance cases and referenced engineering artifacts at both development and runtime, supported by a prototypical dynamic management system.
3. Formal Integration: Facilities to integrate diverse formal verification results (e.g., from Isabelle) into assurance cases and automatically generate formalized assurance cases (Isabelle/SACM) for theorem proving.
4. Change Impact Analysis: Automated analysis of how changes in engineering artifacts impact the assurance case.
5. Practical Application: The successful application of the above to an AUV case study, demonstrating the feasibility of model-based, assurance-centric engineering.

The authors emphasize that ACCESS enables a shift from static, document-based assurance to dynamic, model-driven assurance, which is essential for the safety of adaptive RAS in uncertain environments. They note that while the approach improves efficiency and coverage, future work is needed to address scalability limits and lower the technical barrier for defining validation rules (e.g., by supporting constrained natural languages).