TiPEX: a tool chain for Timed Property Enforcement during eXecution

Abstract. The TiPEX tool implements the enforcement monitoring algorithms for timed properties proposed in [1]. Enforcement monitors are generated from timed automata specifying timed properties. Such monitors correct input sequences by adding extra delays between events. Moreover, 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 paper also presents the performance evaluation of TiPEX within some experimental setup. 1 Enforcement of Timed Properties Runtime enforcement extends runtime verification [2] and refers to the theories, techniques, and tools aiming at ensuring the conformance of the executions of systems under scrutiny w.r.t. some desired property. As shown in Fig. 1, an enforcement moni-tor (EM) modifies an (untrustworthy) input sequence of events into an output sequence that complies with a property. To be as general as possible, we consider that the en-forcement monitor is placed between an event emitter and an event receiver, which can be considered to be e.g., a program or the environment. In [1], we introduced runtime enforcement for timed properties modeled as timed automata. An extensive comparison between runtime enforcement of timed properties and related work is provided in [1]. Enforcement Monitor for ϕ events | = ϕ eventsEven