用形式化验证自动生成机器人软件的安全证据，提升可靠性。
Formal Evidence Generation for Assurance Cases for Robotic Software Models
- 用模板将自然语言需求转为形式化断言
- 集成模型检测与定理证明工具生成证据
- 适合安全关键系统开发团队使用
机器人与自主系统在安全关键领域日益广泛应用，确保其安全性至关重要。保障案例（Assurance Cases, ACs）通过结构化论证和证据支持安全性，但生成与维护证据耗时费力，且随系统演化难以保持一致性。本文提出一种基于模型的方法，将形式化验证嵌入保障流程，系统化生成AC证据。针对三大挑战：利用模板从自然语言需求中自动推导形式化断言；协调多种形式化验证工具以处理不同性质的属性；将形式化证据生成无缝集成至工作流。基于具有形式语义的领域特定建模语言RoboChart，结合模型检测与定理证明技术，实现结构化需求到形式化断言的自动转换，并将验证结果作为证据自动整合。案例研究验证了该方法的有效性。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。