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.

翻译：机器人与自主系统日益部署于安全关键领域，因此证明其安全性至关重要。保证案例通过结构化论证辅以证据支撑，但证据的生成与维护不仅工作繁重、易出错，且难以在系统演进过程中保持一致性。本文提出一种基于模型的方法，通过将形式化验证嵌入保证工作流来系统化生成保证案例证据。该方法应对三大挑战：利用模板从自然语言需求中系统化推导形式化断言，协调多种形式化验证工具以处理多样化的属性类型，以及将形式化证据生产集成至工作流中。借助具备形式语义的领域特定建模语言RoboChart，我们在方法中结合了模型检测与定理证明。结构化需求通过预定义模板自动转换为形式化断言，验证结果则自动整合为证据。案例研究验证了本方法的有效性。