Runtime Enforcement with Event Reordering
摘要
Embedded systems for low latency safety-critical applications such as autonomous vehicles, space flight systems, large-scale chemical, energy and nuclear systems require formal guarantees on the input received at runtime prior to data processing. A common unintended behavior arising in communication over a network is that packets may arrive out-of-order and typically application layer protocols require underlying transport layer packets to arrive in order to ensure Quality of Service (QoS). In this context, if a processor is available to buffer and check events received over the network for safe execution, it is possible to deploy a Runtime Enforcement (RE) framework to guarantee that the protected system receives input that satisfies a set of formally defined properties. However, most current RE frameworks do not consider the order of events while processing their configured policies which makes them less viable to low latency safety-critical applications. This work proposes a new formal RE paradigm which handles event reordering for any regular property specified as an automaton. We formally define the RE framework, develop an online enforcement algorithm, and prove its correctness. We illustrate that our enforcer implementation is latency-sensitive by reasoning about the influence of out-of-order events in all possible future paths. We analyze the limits of memory utilization for enforcement theoretically for a few classes of regular properties along with extensive performance evaluation across a wide range of input lengths and properties. This includes testing the limits of the latency-sensitive implementation and its practical effectiveness against a safety-critical case-study on smart switches.