Formal Evidence Generation for Assurance Cases for Robotic Software Models
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.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Autonomy and Safety Assurance in the Early Development of Robotics and Autonomous Systems
This report provides an overview of the workshop titled Autonomy and Safety Assurance in the Early Development of Robotics and Autonomous Systems, hosted by the Centre for Robotic Autonomy in Demanding and Long-Lasting E…
Autonomous Robotic Swarms: A Corroborative Approach for Verification and Validation
The emergent behaviour of autonomous robotic swarms poses a significant challenge to their safety assurance. Assurance tasks encompass adherence to standards, certification processes, and the execution of verification an…
A causal model of safety assurance for machine learning
This paper proposes a framework based on a causal model of safety upon which effective safety assurance cases for ML-based applications can be built. In doing so, we build upon established principles of safety engineerin…
BIG-bench Machine LearningI came, I saw, I certified: some perspectives on the safety assurance of cyber-physical systems
The execution failure of cyber-physical systems (e.g., autonomous driving systems, unmanned aerial systems, and robotic systems) could result in the loss of life, severe injuries, large-scale environmental damage, proper…
Autonomous DrivingTrusta: Reasoning about Assurance Cases with Formal Methods and Large Language Models
Assurance cases can be used to argue for the safety of products in safety engineering. In safety-critical areas, the construction of assurance cases is indispensable. Trustworthiness Derivation Trees (TDTs) enhance assur…