Compositional runtime enforcement of safety and co-safety timed properties

Runtime enforcement serves as a mechanism to enforce expected properties upon a system, often considered a black box. This is achieved by utilizing an enforcement monitor/enforcer, which transforms an (untrusted) sequence of events into one that conforms to the desired property. Typically, existing frameworks are effective at enforcing a single property. However, when the need arises to enforce multiple properties compositionally, the common practice involves combining these properties by taking their intersection and creating a single enforcement monitor capable of enforcing all these combined properties. Although this approach, known as the monolithic approach, is functional, it does possess certain drawbacks, such as the lack of modularity. Hence, there is a pressing need to construct individual enforcement monitors for each property instead of a monolithic enforcer. These individual enforcement monitors can then be composed accordingly, e.g. serially (one EM after other EM and so on, where the output of one EM serves as the input to the next/succeeding EM in a sequential manner), parallelly (EMs run concurrently, receiving the same input; their individual outputs are then merged using specific methods). Additionally, timed properties offer a more precise means of specifying desired system behaviours by explicitly defining the time intervals between events. Therefore, our research delves into compositional (serial and parallel) monitor composition schemes tailored to safety and co-safety timed properties (modelled as timed automata). We demonstrate that, in general, enforcement monitors for these timed properties do not readily lend themselves to compositional enforcement. We investigate whether, in cases where particular syntactic conditions align with the corresponding timed automata of the properties, their enforcement monitors can be employed in a compositional approach to leverage modular compositional techniques. To provide empirical evidence, we conduct performance evaluations of our framework through a prototype implementation.