Synthesis of Admissible Shields
Synthesis of Admissible Shields
复制标题
可接受屏蔽的合成
DOI：
--
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
U. Topcu
中科院分区：
文献类型：
--
作者：
Laura R. Humphrey;Bettina Könighofer;Robert Könighofer;U. Topcu
盾牌合成是一种在运行时强制反应系统的一组安全性 - 关键特性的方法。盾牌可监视系统并立即纠正任何错误的输出值。盾牌尽快与给定输出偏离了给定的输出，并尽快将控制权交给系统。本文从一项关于无人驾驶汽车（UAV）的案例研究中汲取了灵感，在该案例计划中，K稳定的盾牌（可确保在有限的时间内恢复）无法构建K-Stabilized Shields。我们介绍了可允许的盾牌的概念，该盾牌通过两种方式改善了K稳定的盾牌：（1）而K稳定的盾牌对系统有对抗性的视野，而可允许的盾牌则可以协作。也就是说，如果没有盾牌可以保证在K步骤内恢复，无论系统行为如何，那么可接受的盾牌将尝试与系统合作以尽快恢复。 （2）可接受的盾牌可以在恢复阶段处理系统故障。在我们的实验结果中，我们表明对于无人机，即使不存在K稳定的盾牌，我们也可以产生可允许的盾牌。
Shield synthesis is 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 which k-stabilizing shields, which guarantee recovery in a finite time, could not be constructed. We introduce the notion of admissible shields, which improves k-stabilizing shields in two ways: (1) whereas k-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 within k steps 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 when k-stabilizing shields do not exist.