ロボットソフトウェアモデルの保証ケースに対する形式的証拠生成
Formal Evidence Generation for Assurance Cases for Robotic Software Models
自然言語要求から形式的表明を自動導出し、モデル検査と定理証明を組み合わせて保証ケースの証拠を体系的に生成するモデルベース手法を提案した。
詳しい要約
1. どんなもの？
2. 先行研究と比べてどこがすごい？
3. 技術・手法の肝は？
4. どうやって有効だと検証した？
5. 議論はある？
6. 次に読むべき論文は？
※ AIが要旨から生成した要約です。正確性は原文をご確認ください。
著者: Fang Yan, Simon Foster, Ana Cavalcanti, Ibrahim Habli, James Baxter
分類: cs.SE, cs.FL, cs.LO, cs.RO
原文アブストラクト
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.
