论文标题
安全主管的合理发展
Sound Development of Safety Supervisors
论文作者
论文摘要
安全主管是通过将系统保存（或将其返回）安全状态来执行安全属性的控制器。这种高融合组件的开发可以受益于整合正式设计和验证的严格工作流程。在本文中，我们介绍了一个工作流程，以结合两个世界中最好的安全主管的声音发展，验证的合成和完整的测试。合成使人们可以专注于问题规范和模型验证。测试弥补了抽象，形式主义和工具界限的穿越，并且是在进入服务之前获得认证信贷的关键要素。我们通过严格的论点确定工作流程的健全性。我们的方法是由工具支持的，旨在实现现代自治系统，并以协作机器人的示例进行了说明。
Safety supervisors are controllers enforcing safety properties by keeping a system in (or returning it to) a safe state. The development of such high-integrity components can benefit from a rigorous workflow integrating formal design and verification. In this paper, we present a workflow for the sound development of safety supervisors combining the best of two worlds, verified synthesis and complete testing. Synthesis allows one to focus on problem specification and model validation. Testing compensates for the crossing of abstraction, formalism, and tool boundaries and is a key element to obtain certification credit before entry into service. We establish soundness of our workflow through a rigorous argument. Our approach is tool-supported, aims at modern autonomous systems, and is illustrated with a collaborative robotics example.
