Model-Driven Assurance for Robotic Controllers: A Subterranean Tunnel Inspection Case Study
Autonomous inspection robots operate in hazardous and safety-critical environments where assurance must extend beyond conventional testing. This paper presents a model-driven assurance workflow for the Subterranean Tunnel Autonomous Inspection Robot (ST-AIR), integrating safety, mission, and coordination reasoning within formally verified design models. Behavioural requirements derived from hazard analysis are expressed as formally specified properties and automatically verified through a compositional workflow. The workflow validates individual controllers in isolation and then confirms their synchronised behaviour through integrated harness verification, producing machine-checked evidence of correctness. The verified models capture 29 hazard- and mission-driven behaviours covering gas, water ingress, slope, corrosion, and visibility hazards. Results demonstrate how compositional model verification and structured property templates provide reusable, certification-oriented assurance artefacts that strengthen the dependability of safety-critical autonomous systems.