实用屏蔽合成：在信息物理系统中强制保障安全性
计算机科学中的逻辑
2019-08-16 v1 机器人学
系统与控制
系统与控制
摘要
信息物理系统往往具有安全关键性，因为安全性质的违背可能导致灾难。我们提出一种通过对实值信号系统合成称为屏蔽(shield)的运行时强制器来强制系统安全性的方法。每当系统违背某性质时，与系统组合的屏蔽会瞬时作出修正，以确保组合系统不产生错误输出。尽管布尔屏蔽的合成技术已得到充分理解，但它们无法处理信息物理系统中普遍存在的实值信号，意味着在实域中的修正可能不可实现或计算低效。我们通过静态分析定义在实值信号上的谓词的可兼容性，并利用分析结果约束用于合成屏蔽的双人安全博弈，解决了可实现性与效率问题。我们已实现该方法，并在包括汽车动力总成控制系统在内的多种应用上展示了其有效性与高效性。
引用
@article{arxiv.1908.05402,
title = {Shield Synthesis for Real: Enforcing Safety in Cyber-Physical Systems},
author = {Meng Wu and Jingbo Wang and Jyotirmoy Deshmukh and Chao Wang},
journal= {arXiv preprint arXiv:1908.05402},
year = {2019}
}