On the Runtime Enforcement of Timed Properties

International audienceRuntime enforcement refers to the theories, techniques, and tools for enforcing correct behavior of systems at runtime. We are interested in such behaviors described by specifications that feature timing constraints formalized in what is generally referred to as timed properties. This tutorial presents a gentle introduction to runtime enforcement (of timed properties). First, we present a taxonomy of the main principles and concepts involved in runtime enforcement. Then, we give a brief overview of a line of research on theoretical runtime enforcement where timed properties are described by timed automata and feature uncontrollable events. Then, we mention some tools capable of runtime enforcement, and we present the TiPEX tool dedicated to timed properties. Finally, we present some open challenges and avenues for future work. Runtime Enforcement (RE) is a discipline of computer science concerned with enforcing the expected behavior of a system at runtime. Runtime enforcement extends the traditional runtime verification [12-14, 42, 43] problem by dealing with the situations where the system deviates from its expected behavior. While runtime verification monitors are execution observers, runtime enforcers are execution modifiers. Foundations for runtime enforcement were pioneered by Schneider in [98] and by Rinard in [95] for the specific case of real-time systems. There are several tutorials and overviews on runtime enforcement for untimed systems [39, 47, 59], but none on the enforcement of timed properties (for real-time systems). In this tutorial, we focus on runtime enforcing behavior described by a timed property. Timed properties account for physical time. They allow expressing constraints on the time that should elapse between (sequences of) events, which is useful for real-time systems when specifying timing constraints between statements, their scheduling policies, the completion of tasks, etc [5, 7, 88, 101, 102]. This tutorial comprises four stages: 1. the presentation of a taxonomy of concepts and principles in RE (Sec. 1); 2. the presentation of a framework for the RE of timed properties where specifications are described by timed automata (preliminary concepts are recalled in Sec. 2, the framework is overviewed in Sec. 3, and presented in more details in Sec. 4); 3. the demonstration of the TiPEX [82] tool implementing the framework (Sec. 5); 4. the description of some avenues for future work (Sec. 6)