Shield synthesis
Shield synthesis
复制标题
护盾合成
DOI：
10.1007/978-3-319-49052-6_9
复制
发表时间：
2017
影响因子：
0.8
通讯作者：
Wang, Chao
中科院分区：
文献类型：
--
作者：
Alshiekh, Mohammed;Bloem, Roderick;Humphrey, Laura;Topcu, Ufuk;Wang, Chao
屏蔽综合是一种在运行时强制响应系统的一组安全关键属性的方法。屏蔽监视系统并立即纠正任何错误的输出值。屏蔽尽可能少地偏离给定输出，并尽快恢复将控制交还给系统。本文的研究灵感来自于无法构建保证在有限时间内恢复的稳定护罩的无人机任务规划案例研究。我们引入了容许护盾的概念，它从两个方面改进了稳定护盾：(1)稳定护盾对系统采取对抗的观点，容许护盾采取协作的观点。也就是说，如果不存在能够保证无论系统行为如何都能在5个步骤内恢复的屏蔽，则可接受的屏蔽将尝试与系统一起尽快恢复。(2)容许屏蔽可以在恢复阶段处理系统故障。实验结果表明，对于无人机，即使不存在稳定屏蔽，我们也可以生成允许屏蔽。
Shield synthesisis an approach to enforce a set of safety-critical properties of a reactive system at runtime. A shield monitors the system and corrects any erroneous output values instantaneously. The shield deviates from the given outputs as little as it can and recovers to hand back control to the system as soon as possible. This paper takes its inspiration from a case study on mission planning for unmanned aerial vehicles (UAVs) in whichk-stabilizingshields, which guarantee recovery in a finite time, could not be constructed. We introduce the notion ofadmissibleshields, which improvesk-stabilizingshields in two ways: (1) whereask-stabilizing shields take an adversarial view on the system, admissible shields take a collaborative view. That is, if there is no shield that guarantees recovery withinksteps regardless of system behavior, the admissible shield will attempt to work with the system to recover as soon as possible. (2) Admissible shields can handle system failures during the recovery phase. In our experimental results we show that for UAVs, we can generate admissible shields, even whenk-stabilizing shields do not exist.
登录
查看更多内容
存在活力时的稳健性
DOI：
10.1007/978-3-642-14295-6_36
发表时间：
2010
期刊：
Artif. Intell.
影响因子：
--
作者：
R. Bloem;K. Chatterjee;Karin Greimel;T. Henzinger;Barbara Jobstmann
通讯作者：
Barbara Jobstmann
图上无限博弈中可接受的策略
DOI：
--
发表时间：
2009
期刊：
International Symposium on Mathematical Foundations of Computer Science
影响因子：
--
作者：
M. Faella
通讯作者：
M. Faella
关于将无人机系统集成到国家空域系统中：问题、挑战、操作限制、认证和......以及自动化科学与工程）
DOI：
--
发表时间：
2008
期刊：
影响因子：
--
作者：
K. Dalamagkidis;K. Valavanis;L. Piegl
通讯作者：
L. Piegl
Rabin 和 Streett Games 的更快解决方案
DOI：
10.1109/lics.2006.23
发表时间：
2006
期刊：
21st Annual IEEE Symposium on Logic in Computer Science (LICS'06)
影响因子：
--
作者：
Nir Piterman;A. Pnueli
通讯作者：
A. Pnueli
可接受屏蔽的合成
DOI：
--
发表时间：
2016
期刊：
Haifa Verification Conference
影响因子：
--
作者：
Laura R. Humphrey;Bettina Könighofer;Robert Könighofer;U. Topcu
通讯作者：
U. Topcu