Towards Continuous Assurance with Formal Verification and Assurance Cases

TL;DR

This paper presents a unified Continuous Assurance Framework that combines formal verification and assurance cases to improve the safety and correctness of autonomous systems throughout their lifecycle.

Contribution

It introduces a model-driven, traceable workflow integrating design-time, runtime, and evolution-time assurance, with an Eclipse plugin for automatic assurance argument regeneration.

Findings

Demonstrated on a nuclear inspection robot scenario

Integrated formal methods for functional correctness and probabilistic risk analysis

Ensured traceability and adaptability of assurance arguments

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.