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 & tables
Figure 1: Approach for evidence generation.
Figure 2: Main elements of GSN.
Figure 3: GSN example (adapted from OMG (2021) ).
Figure 4: 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 5: RoboChart state machine Movement .
No.
Requirement
R1
If a dangerous gas is detected, the robot shall flag to report the detection.
R2
Once an obstacle is detected, the location of the obstacle shall be recorded within one time unit.
R3
The chemical detector shall be deadlock-free.
Table 1: Requirements for the Chemical Detector
No.
Claim
Verification Support
C1
Requirement R1 is implemented.
FDR
C2
Requirement R2 is implemented.
FDR
C5
Requirement R3 is implemented.
FDR, Isabelle
Table 2: Example claims for the chemical detector
Requirement category
Description
Untimed safety
Event-based safety constraints defined over untimed behaviour.
Timed safety
Safety requirements involving explicit model-level time, such as bounded-response or deadline constraints.
General correctness
Structural and behavioural correctness properties, including state reachability, software component termination, divergence-freedom, and deadlock-freedom.
Probabilistic properties
Quantitative constraints on event likelihoods or performance measures, including probability thresholds and reward-based expectations.
Temporal properties
Qualitative properties expressed in temporal logics, capturing ordering or eventuality relations between events.
Table 3: Requirement types supported by the proposed framework for RoboChart models.
Requirement Template
Section
Assertion Template
Section
Tool
RT-UNTIMED
Sect. 5.3
AT-UTG
Sect. 6.1
FDR
AT-UTL
Appendix A.2
RT-TIMED
Sect. 5.3
AT-DLINE
Sect. 6.1
FDR
RT-REACH
Appendix A.1
AT-REACH
Appendix. A.2
FDR
RT-DDLK
Sect. 5.3
AT-DDLK-1
Sect. 6.1
FDR
AT-DDLK-2
Isabelle
Table 4: Mapping between requirement templates and the assertion requirements
Figure 6: Excerpt of a RoboTool FDR model-checking report, showing untimed and timed analysis results.
Figure 7: Excerpt of a RoboTool PRISM model-checking report, showing probabilistic analysis results.
Case study
# Assertions
Model size (states / transitions)
Assertion generation (ms)
Evidence generation (ms)
Mail robot (2017)
3
8 / 11
39
56
Painting robot Murray et al. (2022)
4
7 / 10
277
87
Underwater vehicle Yan et al. (2023)
1
5 / 18
580
92
Maintenance robot
4
25 / 35
67
112
Table 5: Summary of the case studies and automation overhead. Model size is given in terms of the number of states and transitions of the RoboChart model. Times are averages over 10 runs in a 1.6 GHz Core i5 computer with 8GB of RAM.
Case study
Requirement Templates (RT)
Assertion Templates (AT)
Mail robot
RT-PROB, RT-RWD, RT-TEMP
AT-PROB, AT-RWD, AT-TEMP
Painting robot
RT-UNTIMED, RT-REACH
AT-UTG, AT-UTL, AT-REACH
Underwater vehicle
RT-DDLK
AT-DDLK-2
Maintenance robot
RT-UNTIMED, RT-REACH, RT-DDLK, RT-DIV
AT-UTG, AT-REACH, AT-DDLK-1, AT-DIV
Table 6: Requirement templates (RT) and assertion templates (AT) used in the case studies.
Figure 8: AC in GSN notation for the mail-delivering robot.
Figure 9: SR1_1_1 exported from Kapture.
Figure 10: SR1_1_2 exported from Kapture.
Figure 11: SR1_1_3 exported from Kapture.
Figure 12: Model checking result for SR1_1_1.
Figure 13: AC module for mail delivery robot updated with formal evidence.
Figure 14: HVC Claim for SR1_2_1.
Figure 15: HVC Claim for SR1_1_1 validation.
Figure 16: HVC assertion for SR1_2_1 verification.
Reference (line of work)
Req. struct.
Assert. gen.
Model transf.
Verif. exec.
Evid. integ.
Trace- ability
Denney & Pai – AutoCert / AdvoCATE Denney and Pai (2018)
✗
✓
✓
✓
✓
✓
Prokhorova et al. – Multi-tool FV (Event-B-centred) Prokhorova et al. (2015)
✗
✗
✗
✓
✓
✗
Bourbouh et al. – Heterogeneous FM (FRET/Lustre/Event-B) Bourbouh et al. (2021) ; Giannakopoulou et al. (2020) ; Mavridou et al. (2025)
✓
✓
✓
✓
✓
✗
Bouskela et al. – FORM-L Bouskela et al. (2022)
✓
✓
✗
✗
✗
✗
Bolton et al. – Template-based LTL Bolton et al. (2014)
✓
✓
✗
✓
✗
✗
Ghosh et al. – ARSENAL Ghosh et al. (2016)
✓
✓
✗
✗
✗
✗
Table 7: Coverage of assurance case workflow stages across related lines of work.
Appendix figures & tables4 assets
Supplementary material from the paper’s appendix.
Appendix
Figure 17: DTI_SR1 requirement in Kapture template
Figure 18: DTI_SR2 requirement in Kapture template
Figure 19: DTI_SR3 requirement in Kapture template
Figure 20: DTI_SR4 requirement in Kapture template
Artificial intelligence assurance develops evidence and controls to evaluate, govern, and certify AI systems across their lifecycle and deployment contexts.