Formal Evidence Generation for Assurance Cases for Robotic Software Models

• URL: http://arxiv.org/abs/2602.03550v1
• Date: Tue, 03 Feb 2026 14:01:30 GMT
• Title: Formal Evidence Generation for Assurance Cases for Robotic Software Models
• Authors: Fang Yan, Simon Foster, Ana Cavalcanti, Ibrahim Habli, James Baxter,
• Abstract summary: Assurance Cases provide structured arguments supported by evidence.<n> generating and maintaining this evidence is labour-intensive, error-prone, and difficult to keep consistent as systems evolve.<n>We present a model-based approach to systematically generating AC evidence by embedding formal verification into the assurance workflow.
• Score: 1.8145248907978841
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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.

Related papers

• Leveraging LLM Parametric Knowledge for Fact Checking without Retrieval [60.25608870901428]
  Trustworthiness is a core research challenge for agentic AI systems built on Large Language Models (LLMs)<n>We propose the task of fact-checking without retrieval, focusing on the verification of arbitrary natural language claims, independent of their source robustness.
  arXiv  Detail & Related papers  (2026-03-05T18:42:51Z)
• BarrierBench : Evaluating Large Language Models for Safety Verification in Dynamical Systems [4.530582224312311]
  We introduce an LLM-based agentic framework for barrier certificate synthesis.<n>The framework uses natural language reasoning to propose, refine, and validate candidate certificates.<n> BarrierBench is a benchmark of 100 dynamical systems spanning linear, nonlinear, discrete-time, and continuous-time settings.
  arXiv  Detail & Related papers  (2025-11-12T14:23:49Z)
• Autoformalizer with Tool Feedback [52.334957386319864]
  Autoformalization addresses the scarcity of data for Automated Theorem Proving (ATP) by translating mathematical problems from natural language into formal statements.<n>Existing formalizer still struggles to consistently generate valid statements that meet syntactic validity and semantic consistency.<n>We propose the Autoformalizer with Tool Feedback (ATF), a novel approach that incorporates syntactic and consistency information as tools into the formalization process.
  arXiv  Detail & Related papers  (2025-10-08T10:25:12Z)
• PAT-Agent: Autoformalization for Model Checking [17.082027022913998]
  PAT-Agent is an end-to-end framework for natural language autoformalization and formal model repair.<n>It combines the generative capabilities of large language models with the rigor of formal verification.
  arXiv  Detail & Related papers  (2025-09-28T06:32:14Z)
• Leveraging LLMs for Formal Software Requirements -- Challenges and Prospects [0.0]
  VERIFAI1 aims to investigate automated and semi-automated approaches to bridge this gap.<n>This position paper presents a preliminary synthesis of relevant literature to identify recurring challenges and prospective research directions.
  arXiv  Detail & Related papers  (2025-07-18T19:15:50Z)
• Justified Evidence Collection for Argument-based AI Fairness Assurance [7.65321625950609]
  This paper introduces a systems-engineering-driven framework, supported by software tooling, to operationalise a dynamic approach to argument-based assurance in two stages.<n>The framework's effectiveness is demonstrated through an illustrative case study in finance, with a focus on supporting fairness-related arguments.
  arXiv  Detail & Related papers  (2025-05-12T21:05:33Z)
• Formal Analysis of the Contract Automata Runtime Environment with Uppaal: Modelling, Verification and Testing [0.11844977816228043]
  A distributed runtime application called contract automata environment (CARE) has been introduced to realise service applications specified using a dialect of finite-state automata.<n>We detail the formal modelling, verification and testing of CARE.
  arXiv  Detail & Related papers  (2025-01-22T15:03:25Z)
• Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
  We introduce SAFE, a framework that overcomes the lack of human-written snippets to enable automated proof generation of Rust code.<n> SAFE re-purposes the large number of synthesized incorrect proofs to train the self-ging capability of the fine-tuned models.<n>We achieve a 52.52% accuracy rate in a benchmark crafted by human experts, a significant leap over GPT-4o's performance of 14.39%.
  arXiv  Detail & Related papers  (2024-10-21T08:15:45Z)
• A General Framework for Verification and Control of Dynamical Models via Certificate Synthesis [54.959571890098786]
  We provide a framework to encode system specifications and define corresponding certificates. We present an automated approach to formally synthesise controllers and certificates. Our approach contributes to the broad field of safe learning for control, exploiting the flexibility of neural networks.
  arXiv  Detail & Related papers  (2023-09-12T09:37:26Z)
• Synthetic Disinformation Attacks on Automated Fact Verification Systems [53.011635547834025]
  We explore the sensitivity of automated fact-checkers to synthetic adversarial evidence in two simulated settings. We show that these systems suffer significant performance drops against these attacks. We discuss the growing threat of modern NLG systems as generators of disinformation.
  arXiv  Detail & Related papers  (2022-02-18T19:01:01Z)
• Joint Differentiable Optimization and Verification for Certified Reinforcement Learning [91.93635157885055]
  In model-based reinforcement learning for safety-critical control systems, it is important to formally certify system properties. We propose a framework that jointly conducts reinforcement learning and formal verification.
  arXiv  Detail & Related papers  (2022-01-28T16:53:56Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.