Formal Evidence Generation for Assurance Cases for Robotic Software Models
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2026
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866908809453109248 |
|---|---|
| author | Yan, Fang Foster, Simon Cavalcanti, Ana Habli, Ibrahim Baxter, James |
| author_facet | Yan, Fang Foster, Simon Cavalcanti, Ana Habli, Ibrahim Baxter, James |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2602_03550 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Formal Evidence Generation for Assurance Cases for Robotic Software Models Yan, Fang Foster, Simon Cavalcanti, Ana Habli, Ibrahim Baxter, James Software Engineering Formal Languages and Automata Theory Logic in Computer Science Robotics 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. |
| title | Formal Evidence Generation for Assurance Cases for Robotic Software Models |
| topic | Software Engineering Formal Languages and Automata Theory Logic in Computer Science Robotics |
| url | https://arxiv.org/abs/2602.03550 |