On the Runtime Enforcement of Timed Properties

The tutorial paper On the Runtime Enforcement of Timed Properties has been accepted for publication in Runtime Verification 2019.

Runtime 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.

This is joint work with Srinivas Pinisetty, IIT Bhubaneswar, India.

The tutorial paper can be downloaded here.