About

Runtime enforcement is a powerful technique to ensure that a running system respects some desired properties. Using an enforcement monitor, an (untrustworthy) input execution (in the form of a sequence of events) is modified into an output sequence that complies to a property. Runtime enforcement has been extensively studied over the last decade in the context of untimed properties.

We are working on runtime enforcement of "timed properties" by revisiting the foundations of runtime enforcement when time between events matters. We propose a new enforcement paradigm where enforcement mechanisms are "time retardants": to produce a correct output sequence, additional delays are introduced between the events of the input sequence.

The TiPEX tool implements enforcement monitoring algorithms for timed properties (see related papers page). An enforcement monitor is generated from a timed automaton specifying a timed property. Its purpose is to correct an input sequence according to this property. In addition, TiPEX also provides modules to generate timed automata from patterns, compose them, and check the class of properties they belong to in order to optimize the monitors.

This website provides details, and references to the papers containing the theoretical results, and more details about the tool implementation, detailing its features, and instructions about how to use. We also provide the source code for download (together with examples).