Enforcement of (Timed) Properties with Uncontrollable Events
Enforcement of (Timed) Properties with Uncontrollable Events
复制标题
具有不可控事件的（定时）属性的强制执行
DOI：
--
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
H. Marchand
中科院分区：
文献类型：
--
作者：
Matthieu Renard;Yliès Falcone;A. Rollet;Srinivas Pinisetty;Thierry Jéron;H. Marchand
本文讨论了具有不可控事件的非计时属性和计时属性的运行时强制。运行时实施在于修改正在运行的系统的执行，以确保它们相对于所需属性的正确性。我们引入了一个框架，该框架将事件字母表上的任何常规计时属性作为输入，其中一些事件是不可控的。无法控制的事件不能被执行机制延迟或拦截。实施机制满足重要的属性，即可靠性和遵从性--这意味着实施机制输出接近输入执行的正确执行。我们讨论了属性在不可控事件下可强制执行的条件，并定义了修改执行以尽快获得正确输出的强制机制。此外，我们在两个抽象级别上综合了运行时强制机制的合理和合规的描述，以便于它们的设计和实现。
This paper deals with runtime enforcement of untimed and timed properties with uncontrollable events. Runtime enforcement consists in modifying the executions of a running system to ensure their correctness with respect to a desired property. We introduce a framework that takes as input any regular timed property over an alphabet of events, with some of these events being uncontrollable. An uncontrollable event cannot be delayed nor intercepted by an enforcement mechanism. Enforcement mechanisms satisfy important properties, namely soundness and compliance - meaning that enforcement mechanisms output correct executions that are close to the input execution. We discuss the conditions for a property to be enforceable with uncontrollable events, and we define enforcement mechanisms that modify executions to obtain a correct output, as soon as possible. Moreover, we synthesise sound and compliant descriptions of runtime enforcement mechanisms at two levels of abstraction to facilitate their design and implementation.