Towards Continuous Assurance with Formal Verification and Assurance Cases
This addresses the problem of maintaining safety and correctness across the lifecycle of autonomous systems, particularly for regulators and developers, but is incremental as it builds on existing formal methods and assurance practices.
The paper tackles the challenge of fragmented assurance in autonomous systems by proposing a Continuous Assurance Framework that integrates design-time, runtime, and evolution-time assurance, demonstrated through formal verification methods on a nuclear inspection robot scenario.
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.