Formal Evidence Generation for Assurance Cases for Robotic Software Models

TL;DR

This work presents a model-based approach that automates evidence generation for Assurance Cases in Robotic Software by embedding formal verification into the AC workflow. It introduces a template-driven pipeline that converts natural-language requirements into tool-ready assertions for CSP (FDR), PRISM (PCTL), and Isabelle, using RoboChart as the modelling backbone and Kapture for requirements. Assertions are automatically verified and their results transformed into SACM-compliant evidence, which is integrated back into the AC, maintaining traceability and consistency as systems evolve. The approach is validated through four robotic case studies, demonstrating substantial automation gains, cross-tool applicability, and scalable integration of formal verification into ACs. This work advances practical AC-based safety assurance by tightly coupling modelling, verification, and evidence management in a coherent, extensible framework.

Abstract

Robotics and Autonomous Systems are increasingly deployed in safety-critical domains, so that demonstrating their safety is essential. Assurance Cases (ACs) provide structured arguments supported by evidence, but generating and maintaining this evidence is labour-intensive, error-prone, and difficult to keep consistent as systems evolve. We present a model-based approach to systematically generating AC evidence by embedding formal verification into the assurance workflow. The approach addresses three challenges: systematically deriving formal assertions from natural language requirements using templates, orchestrating multiple formal verification tools to handle diverse property types, and integrating formal evidence production into the workflow. Leveraging RoboChart, a domain-specific modelling language with formal semantics, we combine model checking and theorem proving in our approach. Structured requirements are automatically transformed into formal assertions using predefined templates, and verification results are automatically integrated as evidence. Case studies demonstrate the effectiveness of our approach.

Figures (19)

• Figure 1: Approach for evidence generation.
• Figure 2: Main elements of GSN.
• Figure 3: Overview of our four-step approach to evidence generation by formal verification. Activities and artefacts within these steps are labelled a - q to allow cross-referencing in the text.
• Figure 4: RoboChart state machine Movement.
• Figure 5: Excerpt of a RoboTool FDR model-checking report, showing untimed and timed analysis results.