Towards Continuous Assurance with Formal Verification and Assurance Cases

TL;DR

Autonomous systems require sustained justification of correctness and safety across design, deployment, and evolution, but traditional assurance yields fragmented, non-adaptive arguments. The paper introduces a Continuous Assurance Framework that unifies design-time verification (RoboChart/FDR4; PRISM) with runtime monitoring and evolution-time regeneration within a model-driven workflow, enabling automatic regeneration of structured assurance artefacts (GSN) as evidence changes. The key contributions are the three-phase framework, the design-time workflow combining RoboChart/FDR4 and PRISM, and the PRISM2GSN pipeline that transforms verification results into traceable assurance arguments, demonstrated on a nuclear radiation inspection robot. This approach enhances traceability, supports lifecycle-spanning oversight, and aligns with regulator-endorsed practices, paving the way for adaptable and auditable assured autonomy.

Abstract

Autonomous systems must sustain justified confidence in their correctness and safety across their operational lifecycle-from design and deployment through post-deployment evolution. Traditional assurance methods often separate development-time assurance from runtime assurance, yielding fragmented arguments that cannot adapt to runtime changes or system updates - a significant challenge for assured autonomy. Towards addressing this, we propose a unified Continuous Assurance Framework that integrates design-time, runtime, and evolution-time assurance within a traceable, model-driven workflow as a step towards assured autonomy. In this paper, we specifically instantiate the design-time phase of the framework using two formal verification methods: RoboChart for functional correctness and PRISM for probabilistic risk analysis. We also propose a model-driven transformation pipeline, implemented as an Eclipse plugin, that automatically regenerates structured assurance arguments whenever formal specifications or their verification results change, thereby ensuring traceability. We demonstrate our approach on a nuclear inspection robot scenario, and discuss its alignment with the Trilateral AI Principles, reflecting regulator-endorsed best practices.

Figures (7)

• Figure 1: Continuous assurance framework with three stages: design-time, runtime, and evolution-time.
• Figure 2: High-level architecture of the nuclear inspection robot and safety wrapper in the case study scenario.
• Figure 3: State machine model of the safety wrapper controller in the case study scenario.
• Figure 4: Navigation state machine model for waypoint navigation in the case study scenario.
• Figure 5: Verifying that the SafetyWrapper_SM state machine is deadlock-free and deterministic.