Specifying Safety Monitors for Autonomous Systems Using Model-Checking
Specifying Safety Monitors for Autonomous Systems Using Model-Checking
复制标题
使用模型检查指定自治系统的安全监视器
DOI：
--
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
H. Waeselynck
中科院分区：
文献类型：
--
作者：
M. Machin;F. Dufossé;J. Blanquart;Jérémie Guiochet;D. Powell;H. Waeselynck
在人类附近运行的自主系统至关重要，因为它们可能会伤害人类。由于自治系统软件的复杂性使得零故障目标很难实现，我们采用了容错的方法。我们考虑一个单独的安全通道，称为监视器，它能够部分观察系统并触发确保安全的动作。介绍了指定安全监控器的系统过程。基于对被监控系统的风险分析，对危险进行正式建模。模型检查器用于综合监控行为规则，以确保被监控系统的安全。通过容许性的概念来解决由于安全监视器的存在而可能过度限制系统功能的问题。已经开发了各种工具来协助这一进程。
Autonomous systems operating in the vicinity of humans are critical in that they potentially harm humans. As the complexity of autonomous system software makes the zero-fault objective hardly attainable, we adopt a fault-tolerance approach. We consider a separate safety channel, called a monitor, that is able to partially observe the system and to trigger safety-ensuring actuations. A systematic process for specifying a safety monitor is presented. Hazards are formally modeled, based on a risk analysis of the monitored system. A model-checker is used to synthesize monitor behavior rules that ensure the safety of the monitored system. Potentially excessive limitation of system functionality due to presence of the safety monitor is addressed through the notion of permissiveness. Tools have been developed to assist the process.