用形式化验证实现系统全生命周期持续可信保障
Towards Continuous Assurance with Formal Verification and Assurance Cases
- 构建统一框架，贯通设计、运行、演化阶段的保障流程
- 结合RoboChart与PRISM验证功能正确性与概率风险
- 自动更新保障论证，适配系统变更，支持监管合规
自主系统需在全生命周期（从设计、部署到后期演进）中持续保持对其正确性与安全性的合理信心。传统保障方法常将开发期与运行期保障割裂，导致论证碎片化，难以应对运行时变化或系统更新，严重制约可信自主。为此，本文提出统一的持续保障框架，将设计期、运行期与演化期保障集成于可追溯的模型驱动流程中，迈向可信自主。具体通过RoboChart实现功能正确性验证，利用PRISM进行概率风险分析，并开发基于Eclipse的模型转换插件，当形式化规格或验证结果变更时自动重生成结构化保障论据，确保全程可追溯。在核设施巡检机器人场景中验证了该方法，其设计符合三边人工智能原则，体现监管认可的最佳实践。
原文摘要 · Abstract (English)
Autonomous systems must sustain justified confidence in their correctness and safety across their operational lifecycle-from design and deployment through post-deployment evolution. Traditional assurance methods often separate development-time assurance from runtime assurance, yielding fragmented arguments that cannot adapt to runtime changes or system updates - a significant challenge for assured autonomy. Towards addressing this, we propose a unified Continuous Assurance Framework that integrates design-time, runtime, and evolution-time assurance within a traceable, model-driven workflow as a step towards assured autonomy. In this paper, we specifically instantiate the design-time phase of the framework using two formal verification methods: RoboChart for functional correctness and PRISM for probabilistic risk analysis. We also propose a model-driven transformation pipeline, implemented as an Eclipse plugin, that automatically regenerates structured assurance arguments whenever formal specifications or their verification results change, thereby ensuring traceability. We demonstrate our approach on a nuclear inspection robot scenario, and discuss its alignment with the Trilateral AI Principles, reflecting regulator-endorsed best practices.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。