减少安全工程师手工工作:面向基于安全模式的自动化安全推理
系统与控制
2020-09-23 v1 密码学与安全
形式语言与自动机理论
计算机科学中的逻辑
系统与控制
摘要
安全关键系统的开发需要控制可能造成伤害的危险。为此,安全工程师在开发阶段依赖称为安全模式的架构解决方案,例如安全监视器、表决器和看门狗。这些模式的目标是控制可能触发危险的(已识别)故障。安全模式可通过例如增加系统冗余来控制此类故障。目前,关于在目标系统哪一部分使用哪种模式来控制哪种危险的推理大多以文本形式或借助模型(如 GSN 模型)记录,对自动化的支持有限。本文提出使用逻辑编程引擎进行系统安全的自动化推理。我们提出一种用于嵌入式系统安全的领域特定语言,并将安全工程师部署安全模式(例如何时使用安全监视器或看门狗)所使用的推理原则表示为析取逻辑程序。我们的机制支持两类自动化安全推理:(1)识别现有安全模式能够控制哪些危险以及不能控制哪些危险;(2)自动推荐在系统何处使用哪些模式以控制潜在危险。最后,我们将我们的机制应用于来自汽车领域的两个示例:自适应巡航控制系统和电池管理系统。
引用
@article{arxiv.2009.10251,
title = {Less Manual Work for Safety Engineers: Towards an Automated Safety Reasoning with Safety Patterns},
author = {Yuri Gil Dantas and Antoaneta Kondeva and Vivek Nigam},
journal= {arXiv preprint arXiv:2009.10251},
year = {2020}
}
备注
In Proceedings ICLP 2020, arXiv:2009.09158