安全监督器的可靠开发

安全监督器是通过使系统保持在（或返回到）安全状态来强制实施安全属性的控制器。此类高完整性组件的开发可受益于集成形式化设计与验证的严谨工作流。在本文中，我们提出了一种用于安全监督器可靠开发的工作流，它结合了验证综合与完备测试两个世界的优点。综合使人能够专注于问题规约与模型验证。测试弥补了抽象、形式化与工具边界的跨越，并且是在投入运行前获得认证信用的关键要素。我们通过严谨的论证确立了工作流的可靠性。我们的方法得到工具支持，面向现代自主系统，并以协作机器人为例进行了说明。