通过形式化验证与保证案例实现持续保证

自主系统必须在其操作生命周期内——从设计和部署到部署后演化——维持对正确性和安全性的合理信心。传统保证方法常将开发时保证与运行时保证分离，导致无法适应运行时变化或系统更新的片段化论证——这对实现可靠自主性构成重大挑战。为此，我们提出一种统一的持续保证框架，将设计时、运行时和演化时保证集成到可追溯、模型驱动的工作流程中，作为实现可靠自主性的一步。本文具体实现了该框架的设计时阶段，采用两种形式化验证方法：RoboChart进行功能正确性验证，PRISM进行概率风险分析。我们还提出一种模型驱动的转换管道，作为Eclipse插件实现，对形式规范或其验证结果变更时自动重新生成结构化保证论证，从而确保可追溯性。我们在核查机器人场景中展示了方法，并讨论了其与三方AI原则的一致性，反映了监管机构认可的最佳实践。