Srinivas Pinisetty

Yliès Falcone
email: ylies.falcone@ujf-grenoble.fr

Thierry Jéron

Hervé Marchand

Antoine Rollet
email: antoine.rollet@labri.fr

Omer Nguena Timo

Falcone, Jéron, Marchand, Rollet Nguena Pinisetty

Timo

Runtime Enforcement of Timed Properties Revisited

Keywords: runtime verification, runtime enforcement, timed properties, timed automata, software engineering

Runtime enforcement is a powerful technique to ensure that a running system satisfies 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 with a property. Over the last decade, runtime enforcement has been mainly studied in the context of untimed properties.

This paper deals with 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. We consider runtime enforcement of any regular timed property defined by a timed automaton. We prove the correctness of enforcement mechanisms and prove that they enjoy two usually expected features, revisited here in the context of timed properties. The first one is soundness meaning that the output sequences (eventually) satisfy the required property. The second one is transparency, meaning that input sequences are modified in a minimal way. We also introduce two new features, i) physical constraints that describe how a time retardant is physically constrained when delaying a sequence of timed events, and ii) optimality, meaning that output sequences are produced as soon as possible. To facilitate the adoption and implementation of enforcement mechanisms, we describe them at several complementary abstraction levels. Our enforcement mechanisms have been implemented and our ex-

Introduction

Runtime verification [START_REF] Thati | Monitoring algorithms for metric temporal logic specifications[END_REF][START_REF] Chen | Parametric trace slicing and monitoring[END_REF][START_REF] Nickovic | From MTL to deterministic timed automata[END_REF][START_REF] Bauer | Runtime verification for LTL and TLTL[END_REF][START_REF] Basin | Algorithms for monitoring real-time properties[END_REF][START_REF] Barringer | Quantified Event Automata: Towards expressive and efficient runtime monitors[END_REF] refers to the theories, techniques, and tools aiming at checking the conformance of the executions of systems under scrutiny w.r.t. some desired property. Runtime enforcement [START_REF] Schneider | Enforceable security policies[END_REF][START_REF] Ligatti | Run-time enforcement of nonsafety policies[END_REF][START_REF] Falcone | You should better enforce than verify[END_REF][START_REF] Falcone | Runtime enforcement monitors: composition, synthesis, and enforcement abilities[END_REF] extends runtime verification 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. The first step of monitoring approaches consists in instrumenting the underlying system so as to partially observe the events or the parts of its global state that may influence the property under scrutiny. A central concept is the verification or enforcement monitor that is generally synthesized from the property expressed in a high-level formalism. Then, the monitor can operate either online by receiving events in a lock-step manner with the execution of the system or offline by reading a log/sequence of system events/actions. When the monitor is only dedicated to verification, it is a decision procedure emitting verdicts stating the correctness of the (partial) observed trace generated from the system execution. When the monitor additionally has enforcement abilities, it corrects any incorrect execution to meet a desirable behavior (and leaves correct executions unchanged).

Three categories of runtime verification frameworks can be distinguished according to the formalism used to express the input property. In propositional approaches, properties refer to events taken from a finite set of propositional names. For instance, a propositional property may rule the ordering of function calls in a program. Monitoring such kind of properties has received a lot of attention. Parametric approaches have received a growing interest in the last five years. In this case, events in the property are augmented with formal parameters, instantiated at runtime. In timed approaches, the observed time between events may influence the truth-value of the property. It turns out that monitoring of timed properties (where time is continuous) is a much harder problem because of (at least) two reasons. First, modeling timed requirements requires a more complex formalism involving time as a continuous parameter. Second, when monitoring a timed property, the problem that arises is that the overhead induced by the monitor (i.e., the time spent executing the monitoring code) influences the truth-value of the monitored property. Consequently, without assumptions and limitations on the computation performed by monitors (see § Context and Objectives), not much information can be gained from the verdicts produced by the monitor. Few attempts have been made on monitoring systems w.r.t. timed properties (see Sec. 5 for a detailed comparison with related work). Roughly speaking, two lines of work can be distinguished: synthesis of automata-based decision procedures for timed formalisms (e.g., [START_REF] Thati | Monitoring algorithms for metric temporal logic specifications[END_REF][START_REF] Nickovic | From MTL to deterministic timed automata[END_REF][START_REF] Bauer | Runtime verification for LTL and TLTL[END_REF][START_REF] Basin | Algorithms for monitoring real-time properties[END_REF]), and, tools for runtime verification of timed properties [START_REF] Nickovic | AMT: a property-based monitoring tool for analog systems[END_REF][START_REF] Colombo | LARVA -safer monitoring of real-time Java programs (tool paper)[END_REF].

In runtime enforcement, an enforcement monitor (EM) is used to transform some (possibly) incorrect execution sequence into a correct sequence w.r.t. the property of interest. In the propositional case, the transformation performed by an EM should be sound and transparent. Soundness means that the resulting sequence obeys the property. Transparency historically means that, the monitor should modify the input sequence in a minimal way (meaning that the input sequence should not be modified if it already conforms to the property). According to how a monitor is allowed to modify the input sequence (i.e., the primitives afforded to the monitor), several models of enforcement monitors have been proposed [START_REF] Schneider | Enforceable security policies[END_REF][START_REF] Ligatti | Run-time enforcement of nonsafety policies[END_REF][START_REF] Falcone | You should better enforce than verify[END_REF][START_REF] Falcone | Runtime enforcement monitors: composition, synthesis, and enforcement abilities[END_REF]. In a nutshell, an EM can definitely block the input sequence (as done by security automata [START_REF] Schneider | Enforceable security policies[END_REF]), suppress an event from the input sequence (as done by suppression automata [START_REF] Ligatti | Run-time enforcement of nonsafety policies[END_REF]), insert an event to the input sequence (as done by insertion automata [START_REF] Ligatti | Run-time enforcement of nonsafety policies[END_REF]), or perform any of these primitives (as is the case with edit-automata [START_REF] Ligatti | Run-time enforcement of nonsafety policies[END_REF] or so-called generalized enforcement monitors [START_REF] Falcone | Runtime enforcement monitors: composition, synthesis, and enforcement abilities[END_REF]). Moreover, according to how transparency is effectively formalized, several definitions of runtime enforcement have been proposed (see [START_REF] Falcone | You should better enforce than verify[END_REF] for an overview). The notion of time has been considered in previous runtime enforcement approaches such as in [START_REF] Matteucci | Automated synthesis of enforcing mechanisms for security properties in a timed setting[END_REF] for discrete-time properties, and in [START_REF] Basin | Enforceable security policies revisited[END_REF] which considers elapsing of time as a series of uncontrollable events ("ticks").

Context and Objectives. The general context is depicted in Fig. 1. We focus on online enforcement of timed properties. More specifically, given a timed property ϕ, we synthesize an enforcement mechanism that operates at runtime. To be as general as possible, an enforcement mechanism is supposed to be placed between an event emitter and an event receiver. The emitter and receiver execute asynchronously. Note, this abstract architecture is generic and can be instantiated to many concrete ones where the emitter and receiver are considered to be e.g., a program or the environment. In all cases, we assume that delaying an event from the emitter does not effect its subsequent events. This assumption is reasonable in many practical application scenarios with architectures compatible with the one described above.

An enforcement mechanism inputs a sequence of timed event σ and transforms it into a sequence of timed events o. No constraint is required on σ, whereas the enforcement mechanism ensures that o is correct w.r.t. property ϕ. Satisfaction of property ϕ by the output sequence is considered at the output of the enforcement mechanism and not at the input of the event receiver: we assume a reliable, without delay, and safe communication between the emitter and receiver. As usual in runtime enforcement, we do not consider any security, communication, nor reliability issue with events. The considered enforcement mechanisms are time retardants, i.e., their main enforcement primitive consists in delaying the received events. Contrary to edit-automata, enforcement mechanisms, as considered in this paper, are not able to generate nor suppress events because of i) inducing more costly computations in a timed context, and ii) delaying events is already sufficient in many application domains. Since time between events matters, we assume the enforcement mechanism to be infinitely faster than the emitter and receiver. In other words, the computation time of the enforcement mechanism is negligible: at runtime, the computation performed by the enforcement mechanism is done in zero-time. 1 Moreover, we assume that delaying the events of the emitter does not influence its behavior.

To sum up, given some timed property ϕ and an input timed word σ, we aim to study mechanisms that input σ and output a sequence o that i) satisfies ϕ (soundness of the mechanism), ii) has the same order of events as σ with possibly increased delays (transparency of the mechanism), iii) is released as fast as possible (optimality of the mechanism). 2Motivations. To the best of our knowledge, no approach focusing on enforcement of timed properties has been proposed. Motivations for extending runtime enforcement to timed properties abound. First, timed properties are more precise to specify desired behaviors of systems since they allow to explicitly state how time should elapse between events. Thus, timed properties/specifications can be particularly useful in some application domains [START_REF] Pinisetty | Runtime enforcement of parametric timed properties with practical applications[END_REF]. For instance, in the context of security monitoring, enforcement monitors can be used as firewalls to prevent denial of service attacks by ensuring a minimal delay between input events (carrying some request for a protected server). On a network, enforcement monitors can be used to synchronize streams of events together, or, ensuring that a stream of events conforms to the pre-conditions of some service.

The following requirements could specify the expected behavior of a server:

R 1 "There should be a delay of at least 5 time units between any two user requests (r)". R 2 "The user should perform a successful authentication, that is, he should send a request (r) and receive a grant (g) between 10 and 15 time units". R 3 "Resource grants (g) and releases (r) should alternate, starting with a grant, and every grant should be released within 15 to 20 time units". R 4 "Every 10 time units, there should be a request for a resource followed by a grant. The request should occur within 5 time units".

R 1 (resp. R 2 ) can be formalized as a safety (resp. co-safety) property. Safety (resp. cosafety) properties express that "something bad should never happen" (resp. "something good should happen within a finite amount of time"). Moreover, in the space of regular properties (over timed words), many interesting properties of systems are neither safety nor co-safety properties that typically specify some form of transactional behavior. Such behaviors are illustrated by requirements R 3 and R 4 . In this paper, we propose to synthesize enforcement mechanisms for all regular timed properties.

Some motivating examples illustrating enforcement mechanisms. Let us consider again requirements R 1 and R 3 . In Sec. 2 we will describe how to formalize these requirements as properties defined by timed automata. Before going further into the formal definitions, we briefly describe how an enforcement mechanism corrects an input sequence to satisfy a property. To enforce the properties, the enforcement mechanism is placed at the input of the server and operates on command-messages that it receives (destinated to the server). The enforcement mechanism releases the (correct sequence of) command-messages into the server input. In the following discussion of the examples, t denotes the current instant of time, i.e., the total time since the beginning of the considered sequence. Let us consider requirement R 1 . Let r and a be the possible actions where r denotes request of a resource. We now illustrate how an enforcement mechanism corrects the input sequence σ = (1, a) • (3, r) • (1, r) (where each event is associated with a delay, indicating the time elapsed after the previous event or the system initialization for the first event). The monitor receives the first action a at t = 1. Since, the safety requirement is not violated, the monitor outputs it immediately (the mechanism is sound and optimal as it ouput a correct sequence which is delayed in a minimal way). The second action r is received by the monitor at t = 4, and the monitor outputs it immediately. The last action r, is received at t = 5. If the action is output immediately, then the safety requirement would be violated (since only 1 time unit has elapsed after the monitor output the previous r action), and thus the mechanism would not be sound anymore. Thus, to satisfy R 1 , the monitor outputs the last r action at t = 9, introducing a delay of 4 time units (which is the minimal required delay as per optimality requires). The output of the monitor is (1, a) • (3, r) • (5, r). Note that the order of actions is preserved, only the delays between them have been possibly augmented.

Let us now consider requirement R 3 . Recall that g and r are the actions denoting the grant and release of the resource, respectively. We illustrate how an enforcement monitor corrects the input sequence σ = (3, g) • (10, r) • (3, g) • (5, g). The monitor receives the first action g at t = 3, the second action r at t = 13, etc. The monitor cannot output the first received action g because the event alone does not satisfy the requirement (and the monitor does not know yet the next events). If the next event is r, then it can output the events g followed by r, if it can choose good delays for both the events satisfying the timing constraints. At t = 13, the monitor can decide that the first two events can be released as output. Hence in output, the delay associated with the first g is 13 t.u. If the monitor should choose the same delay for the second action r, then the property cannot be satisfied. The monitor chooses a delay of 15 t.u. which is the minimal delay satisfying the constraint that is greater than the corresponding delay in the input sequence. When the monitor observes the second g at t = 16, it releases it as output, and again waits for the next event. Since the next input event observed at t = 21 is not r, the sequence violates the property and cannot be corrected by the monitor. Hence, after t = 21, the output of the monitor remains (13, g) • (15, r).

Contributions. We introduce runtime enforcement of timed properties. For this purpose, we adapt soundness and transparency to a timed context. We show how to synthesize runtime enforcement mechanisms for any regular property defined by a timed automaton. In contrast with previous runtime enforcement approaches [START_REF] Ligatti | Run-time enforcement of nonsafety policies[END_REF][START_REF] Schneider | Enforceable security policies[END_REF][START_REF] Falcone | Runtime enforcement monitors: composition, synthesis, and enforcement abilities[END_REF], our mechanisms only have the primitive of being able to delay input events so that the output sequence conforms to the property. To ease the design and implementation of enforcement monitors, we describe them at several abstraction levels: the notion of enforcement function describes the behavior of an enforcement mechanism at an abstract level as an input-output relation between timed words. An enforcement monitor implements an enforcement function and describes the behavior of an enforcement mechanism in an operational way as a rule-based transition system. Enforcement algorithms describe the implementation of enforcement monitors and serve to guide the concrete implementation of enforcement mechanisms. The difficulty that arises when considering regular properties is that the aforementioned enforcement mechanisms should consider input (corrected) sequences of events that alternate between satisfying and not satisfying the underlying property. Experiments have been performed on prototype monitors to show their effectiveness and the feasibility of our approach.

This paper combines and extends the results of the two papers [START_REF] Pinisetty | Runtime enforcement of timed properties[END_REF][START_REF] Pinisetty | Runtime enforcement of regular timed properties[END_REF]. More specifically, this paper provides the following additional contributions:

to propose a more complete and revised theoretical framework for runtime enforcement of timed properties: we have re-visited the notations, unified and simplified the main definitions;

to propose a completely new implementation of our enforcement monitors that i) offers better performance (compared to the ones in [START_REF] Pinisetty | Runtime enforcement of timed properties[END_REF]), ii) are now loosely-coupled to UPPAAL; to synthesize and evaluate enforcement monitors for more properties on longer executions; to include correctness proofs of the proposed mechanisms. Importantly, while our synthesis techniques yield sound, transparent, and optimal enforcement mechanisms for all regular properties, some input execution sequences, while being correct, are not producible by our enforcement mechanisms. Indeed, we exhibit a notion of what we refer to as non-enforceable properties, for which physical time constraints prevent the associated enforcement mechanisms from preserving correct sequences. Intuitively, such undesired situation occurs when enforcing for instance co-safety properties: while the enforcement mechanism reads a correct input sequence, at the moment when it receives the event that allows it to determine that the sequence is correct, it is not possible anymore to release the first read event because the delay of the first event is now greater than the maximal value allowed by the guard on the corresponding transition in the underlying timed automaton. As we shall see, requirement R 4 can be formalized as a so-called non-enforceable timed property (Remark 3).

Paper organization. Section 2 introduces preliminaries and notation and also explains how properties are defined as timed automata on some examples. Section 3 details the enforcement mechanisms (enforcement function, monitor, and algorithm). Our prototype implementations of monitors and experiments are presented in Sec. 4. Section 5 discusses related work. Finally, conclusions and open perspectives are drawn in Sec. 6. To facilitate the reading of this paper, after each proposition we propose a sketch of proof. Full versions of the proofs along with some further notation required for the proofs are available in Appendix A.

Preliminaries and Notation

Untimed Notions

N denotes the set of non-negative integers. An alphabet is a set of elements. A (finite) word over an alphabet A is a finite sequence of elements of A. The length of a word σ is denoted as |σ|. The empty word over A is denoted by A or when clear from the context. The set of all (respectively non-empty) finite words over A is denoted by A * (respectively A + ). A language over A is a set L ⊆ A * . The concatenation of two words σ and σ is denoted by σ • σ . The empty word over A is neutral for concatenation of words of A: ∀σ ∈ A * :

σ • A def = A • σ def = σ.
A word σ is a prefix of a word σ, denoted as σ σ, whenever there exists a word σ such that σ = σ • σ , and σ is a strict prefix of σ denoted as σ ≺ σ whenever σ σ ∧ |σ | < |σ|. For a word σ and

1 ≤ i ≤ |σ|, the i-th letter (resp. prefix of length i, suffix starting at position i) of σ is denoted σ(i) (respectively σ [•••i] , σ [i••• ] ) - with the convention σ [•••0] def = .
Given a word σ and two integers i, j, such that i ≤ j and |σ| ≥ j, the sub-word from index i to j is defined as

σ [i•••j] def = σ [•••j][i••• ]
. Given a word σ, the last letter, σ(|σ|), is denoted last(σ). The set pref(σ) denotes the set of prefixes of σ and by extension, pref(L) def = {pref(σ) | σ ∈ L} is the set of prefixes of words in L. A language L is said to be prefix-closed whenever pref(L) = L and extension-closed whenever L = L•A * . Given an n-tuple of symbols e = (e 1 , . . . , en), Π i (e) is the projection of e on its i th element (Π i (e) def = e i ). The projection function is extended to sequences of tuples in the standard way.

Timed Languages and Properties as Timed Automata

Let R ≥0 denote the set of non-negative real numbers, and Σ a finite alphabet of actions. A pair (δ, a) ∈ (R ≥0 × Σ) is called an event. We note delay(δ, a) def = δ and act(δ, a) = a the projections of events on delays and actions, respectively. A timed word over Σ is a finite sequence of events ranging over (R ≥0 ×Σ) * . A timed language is any set L ⊆ (R ≥0 ×Σ) * . We consider a timed word σ = (δ 1 , a 1 )

• (δ 2 , a 2 ) • • • (δn, an). For i ∈ [2, n
], δ i is the delay between a i-1 and a i , and, δ 1 the time elapsed before the first action a 1 . Note that even though the alphabet (R ≥0 × Σ) is infinite in this case, previous notions and notations defined above (related to length, concatenation, prefix, etc) naturally extend to timed words. The untimed projection

of σ is Π Σ (σ) def = a 1 • a 2 • • • an in Σ * (i.e.
, delays are ignored). The duration of a timed word σ, denoted by time(σ) def = Σ n i=1 δ i , is the sum of its delays.

Timed automata. A timed automaton [START_REF] Alur | A theory of timed automata[END_REF] is a finite automaton extended with a finite set of real valued clocks.

Let X = {x 1 , . . . , x k } be a finite set of clocks. A clock valuation for X is a function ν from X to R ≥0 . R X ≥0 denotes the valuations of clocks in X. For ν ∈ R X ≥0 and δ ∈ R ≥0 , ν + δ is the valuation assigning ν(x) + δ to each clock x of X. Given a set of clocks X ⊆ X, ν[X ← 0]
is the clock valuation ν where all clocks in X are assigned to 0. G(X) denotes the set of clock constraints defined as Boolean combinations of simple constraints of the form x c with x ∈ X, c ∈ N and ∈ {<, ≤, =, ≥, >}. Given g ∈ G(X) and ν ∈ R X ≥0 , we write ν |= g when g holds according to ν.

Definition 1 (Timed automata) A timed automaton (TA) is a tuple A = (L, l 0 , X, Σ, ∆, G), such that L is a finite set of locations with l 0 ∈ L the initial location, X is a finite set of clocks, Σ is a finite set of actions,

∆ ⊆ L × G(X) × Σ × 2 X × L is the transition relation. G ⊆ L is a set of accepting locations.
The semantics of a TA is a timed transition system

[[A]] = (Q, q 0 , Γ, →, F G ) where Q = L × R X
≥0 is the (infinite) set of states, q 0 = (l 0 , ν 0 ) is the initial state where ν 0 is the valuation that maps every clock in X to 0,

F G = G × R X
≥0 is the set of accepting states, Γ = R ≥0 × Σ is the set of transition labels, i.e., pairs composed of a delay and an action.

The transition relation

→⊆ Q × Γ × Q is a set of transitions of the form (l, ν) (δ,a) ---→(l , ν ) with ν = (ν + δ)[Y ← 0] whenever there exists (l, g, a, Y, l ) ∈ ∆ such that ν + δ |= g for δ ∈ R ≥0 .
In the following, we consider a timed automaton A = (L, l 0 , X, Σ, ∆, G) with its semantics [[A]]. A is deterministic whenever for any two distinct transitions (l, g 1 , a, Y 1 , l 1 ) and (l, g 2 , a, Y 2 , l 2 ) in ∆, g 1 ∧ g 2 is unsatisfiable. A is complete whenever for any location l ∈ L and any action a ∈ Σ, the disjunction of the guards of the transitions leaving l and labeled by a evaluates to true (i.e., it holds according to any valuation). In the remainder of this paper, we shall consider only deterministic timed automata, and, automata refer to timed automata.

Remark 1 (Completeness and determinism) In this paper, we restrict the presentation to deterministic TAs. However, results also hold for non-deterministic TAs, with slight adaptations required to the vocabulary and when synthesizing an enforcement monitor. Regarding completeness, if no transition can be triggered upon the reception of an event, a TA implicitly moves to a non-accepting trap state (i.e., a state with no successor).

A run ρ from q ∈ Q is a sequence of moves in [[A]]: ρ = q (δ1,a1) -----→ q 1 • • • q n-1 (δn,an) -----→ qn,
for some n ∈ N. The set of runs from q 0 ∈ Q is denoted Run(A) and Run F G (A) denotes the subset of runs accepted by A, i.e., when qn ∈ F G . The trace of a run ρ is the timed word (δ 1 , a 1 ) • (δ 2 , a 2 ) • • • (δn, an). We note L(A) the set of traces of Run(A). We extend this notation to L F G (A) in a natural way.

Regular, safety, and co-safety timed properties. In the sequel, we shall be interested in the set of regular timed properties, i.e., the timed properties that can be defined by a TA. Within the set of regular timed properties, we are interested in safety and co-safety properties. Informally, safety (resp. co-safety) properties state that "nothing bad should ever happen" (resp. "something good should happen within a finite amount of time"). In this paper, the classes are characterized as follows:

Definition 2 (Regular, safety, and co-safety properties) -Regular properties are the properties that can be defined by languages accepted by a TA.

-Safety properties (a subset of regular properties) are the non-empty prefix-closed timed languages (i.e., the languages L s.t. pref(L) = L), that can be defined by a TA. -Co-safety properties (a subset of regular properties) are the non-universal extensionclosed timed languages (i.e., the languages L s.t. L = L • A * ), that can be defined by a TA.

Remark 2 Usually, safety properties are defined as prefix-closed languages, and co-safety as extension-closed languages. With the usual definitions, the two properties ∅ and (R ≥0 × Σ) * (the empty and universal properties, respectively vacuously and universally satisfied) are both, at the same time safety and co-safety properties, and are the only ones in the intersection. In this paper, to simplify the presentation and to avoid pathological cases, we separate the two classes, by considering that (R ≥0 × Σ) * is a safety (but not a co-safety) property, and ∅ is a co-safety (but not a safety) property.

Safety and co-safety timed automata. In the sequel, we shall only consider the properties that can be defined by a deterministic timed automaton (Definition 1). Note that some of these properties can be defined using a timed temporal logic such as a subclass of MTL, which can be transformed into timed automata using the technique described in [START_REF] Maler | From MITL to timed automata[END_REF][START_REF] Nickovic | From MTL to deterministic timed automata[END_REF]. We now define how to determine whether a regular property defined by a TA defines a safety or a co-safety property by examining its transition relation. Definition 3 (Safety and co-safety TA) A complete and deterministic TA (L, l 0 , X, Σ, ∆, G), where G ⊆ L is the set of accepting locations, is said to be: It is easy to check that safety and co-safety TAs define safety and co-safety properties. 3Example 1 ((Safety and co-safety) timed automata) We consider requirements R 1 , R 2 , R 3 , and R 4 , introduced in Sec. 1. These requirements are respectively formalized as properties ϕ 1 , ϕ 2 , ϕ 3 , and ϕ 4 defined by the timed automata in Fig. 2. Accepting locations are denoted by squares. The safety TA in Fig. 2a defines property ϕ 1 defined over Σ 1 = {a, r}. The co-safety TA in Fig. 2b defines property ϕ 2 defined over Σ 2 = {r, g, a}. The TA in Fig. 2c defines property ϕ 3 defined over Σ 3 = {r, g}. The TA in Fig. 2d defines property ϕ 4 defined over Σ 4 = {r, g}.

-a safety TA if l 0 ∈ G ∧ (l, g, a, Y, l ) ∈ ∆ : l ∈ L \ G ∧ l ∈ G; -a co-safety TA if l 0 / ∈ G ∧ (l, g, a, Y, l ) ∈ ∆ : l ∈ G ∧ l ∈ L \ G.
Combining properties using Boolean operations. The next definition, as described in [START_REF] Alur | A theory of timed automata[END_REF], provides a way to combine (complete and deterministic) timed automata and will be used in the sequel to define properties expressed as a Boolean combination of other properties.

Definition 4 (Operations on timed automata) Given two properties ϕ 1 and ϕ 2 defined by TAs

Aϕ 1 = (L 1 , 0 1 , X 1 , Σ, ∆ 1 , G 1 ) and Aϕ 2 = (L 2 , 0 2 , X 2 , Σ, ∆ 2 , G 2 )
, respectively. The ×op-product of Aϕ 1 and Aϕ 2 , where op ∈ {∪, ∩}, is the timed automaton defined as

Aϕ 1 ×op Aϕ 2 def = (L, l 0 , X, Σ, ∆, G) where L = L 1 × L 2 , l 0 = (l 1 0 , l 2 0 ), X = X 1 ∪ X 2 (disjoint union), ∆ ⊆ L × G(X) × Σ × 2 X × L is the transition relation, where ((l 1 , l 2 ), g 1 ∧ g 2 , a, Y 1 ∪ Y 2 , (l 1 , l 2 )) ∈ ∆ iff (l 1 , g 1 , a, Y 1 , l 1 ) ∈ ∆ 1 and (l 2 , g 2 , a, Y 2 , l 2 ) ∈ ∆ 2 .
Gop is a set of accepting locations with:

-G∩ = G 1 × G 2 , -G∪ = (L 1 × G 2 ) ∪ (G 1 × L 2 ).
Definition 5 (Negation of a timed automaton) Given a property ϕ defined by a TA Aϕ = (L, 0 , X, Σ, ∆, G) its negation is defined as

¬Aϕ def = (L, 0 , X, Σ, ∆, L \ G).
The proposition below states that when performing the ∩-product (resp. ∪-product) between two TAs, it amounts to perform the intersection (resp. union) of the recognized languages.

Proposition 1 Consider two properties ϕ 1 and ϕ 2 defined by TAs

Aϕ 1 = (L 1 , 0 1 , X 1 , Σ, ∆ 1 , G 1 ) and Aϕ 2 = (L 2 , 0 2 , X 2 , Σ, ∆ 2 , G 2 )
, respectively. The following facts hold:

-L (Aϕ 1 ×∩Aϕ 2 )(G∩) = ϕ 1 ∩ ϕ 2 , -L (Aϕ 1 ×∪Aϕ 2 )(G∪) = ϕ 1 ∪ ϕ 2 , -L ¬Aϕ 1 = (R ≥0 × Σ 1 ) * \ L (Aϕ 1 ) , -L ¬Aϕ 2 = (R ≥0 × Σ 2 ) * \ L (Aϕ 2 ) .
The above proposition entails that the classes of safety and co-safety properties are closed under union and intersection. However, the properties resulting of any other operation between safety, co-safety, and regular properties is a regular property. Finally, note that the negation of a safety (resp. co-safety) property is a co-safety (resp. safety) property. From the results shown in [START_REF] Alur | A theory of timed automata[END_REF], the following proposition holds.

Proposition 2 (Closure of safety, co-safety and regular properties under Boolean operations) -Safety and co-safety properties are closed under (finite) union and intersection.

-The negation of a safety property is a co-safety property, and vice-versa.

-Regular properties are closed under Boolean operations.

Preliminaries to Runtime Enforcement

Given t ∈ R ≥0 , and a timed word σ ∈ (R ≥0 × Σ) * , we define the observation of σ at time t as the timed word:

obs(σ, t) def = max {σ ∈ (R ≥0 × Σ) * | σ σ ∧ time(σ ) ≤ t},
where max takes the maximal sequence according to the prefix ordering (unique in this case). That is obs(σ, t) is the longest prefix of σ of duration smaller than t. By definition, time(obs(σ, t)) ≤ t, meaning that the duration of an observation at time t never exceeds t.

The maximal strict prefix of σ that belongs to ϕ is denoted as max ϕ ≺, (σ) and defined as: max ϕ ≺, (σ)

def = max {σ ∈ (R ≥0 × Σ) * | σ ≺ σ ∧ σ ∈ ϕ} ∪ { } .
Orders on timed words. Apart from the prefix order , we define the following partial orders on timed words:

Delaying order d : For σ, σ ∈ (R ≥0 × Σ) * , we say that σ delays σ (denoted

σ d σ) iff Π Σ (σ ) Π Σ (σ) and ∀i ≤ |σ | : delay(σ(i)) ≤ delay(σ (i)),
which means that σ is "a delayed prefix" of σ. This order will be used to characterize outputs w.r.t. to inputs in enforcement monitoring. Lexical order lex : Given any two timed words σ, σ with same untimed projection, i.e., Π Σ (σ) = Π Σ (σ ), and any two timed events with identical actions (δ, a) and (δ , a), we define lex inductively as follows:

lex , and (δ, a)

• σ lex (δ , a) • σ iff δ ≤ δ ∨ (δ = δ ∧ σ lex σ
). This ordering is defined for timed words with identical actions, and is useful to choose a unique timed word among some with same actions.

Enforcement Monitoring in a Timed Context

Roughly speaking, the purpose of enforcement monitoring is to read some (possibly incorrect) input sequence produced by a running system (input to the enforcement mechanism), and to transform it into an output sequence that is correct w.r.t. a property ϕ. To ease the design and implementation of enforcement monitoring mechanisms in a timed context, we introduce two sorts of mechanisms: enforcement functions and enforcement monitors. From an abstract point of view, an enforcement function describes the transformation of an input timed word into an output timed word according to time. An enforcement monitor is a transition system, whose input/output behavior realizes an enforcement function. In other words, an enforcement function serves as an abstract description (black-box view) of an enforcement monitor, and, an enforcement monitor is an operational description of an enforcement function.

Enforcement Functions

The input of an enforcement function is considered to be a timed word σ where every action is associated to the delay since the previous action (or the initialization). Moreover, at this abstract level, even if σ is partially known, it is considered to be fully determined from the beginning. At time t, the sequence observed by the enforcement mechanism is obs(σ, t). The output of the enforcement function at time t should be a timed word representing a sequence of actions with delays between them computed from obs(σ, t).

Definition 6 (Enforcement function) An enforcement function for a property

ϕ is a func- tion Eϕ from (R ≥0 × Σ) * × R ≥0 to (R ≥0 × Σ) * . Enforcement function ϕ, t
Eϕ(σ, t) σ An enforcement function Eϕ for property ϕ transforms some (possibly incorrect) timed word σ given as input (see Fig. 3). In this paper, we assume that enforcement mechanisms do not modify the actions they receive but are rather time retardants, i.e., their output at time t is a timed word Eϕ(σ, t) with same actions as a prefix of their observation, but with possibly increased delays between actions, in such a way that the output timed word satisfies the property.

Constraints on enforcement functions. Similarly to the untimed setting, several constraints, namely soundness and transparency, are required on how Eϕ transforms timed words. Since our enforcement monitors are time retardants, the physical constraints in the following definition also apply to Eϕ.

Definition 7 (Constraints on an Enforcement Mechanism) For a timed property ϕ, an enforcement mechanism behaves as a function Eϕ from (R ≥0 × Σ) * × R ≥0 to (R ≥0 × Σ) * , satisfying the following constraints:

-Physically time retardant:

∀σ ∈ (R ≥0 × Σ) * , ∀t, t ∈ R ≥0 : t ≤ t =⇒ Eϕ(σ, t) Eϕ(σ, t ) (Phy1). ∀σ ∈ (R ≥0 × Σ) * , ∀t ∈ R ≥0 : time(Eϕ(σ, t)) ≤ t (Phy2).
-Soundness:

∀σ ∈ (R ≥0 × Σ) * , ∀t ∈ R ≥0 : Eϕ(σ, t) = =⇒ (∃t ≥ t : Eϕ(σ, t ) |= ϕ) (Snd).
-Transparency:

∀σ ∈ (R ≥0 × Σ) * , ∀t ∈ R ≥0 : Eϕ(σ, t) d obs(σ, t) (Tr).
The requirements on the enforcement function are specified by three constraints: physically time retardant, soundness, and transparency. (Phy1) means that the outputs of the enforcement function are concatenated over time, i.e., what is output cannot be modified.

(Phy2) expresses that the duration of the output never exceeds t. Soundness (Snd) means that if a timed word is released as output by the enforcement function, in the future, the output of the enforcement function should satisfy property ϕ. In other words, no event is output before being sure that the property will be satisfied by subsequent events. In the particular case of a safety property ϕ, since ϕ is prefix closed, soundness reduces to

∀σ ∈ (R ≥0 × Σ) * , ∀t ∈ R ≥0 : Eϕ(σ, t) |= ϕ.
Transparency (Tr) expresses that, at any time t, the output is a delayed prefix of the observed input obs(σ, t).

Functional Definition

We propose first a general definition of an enforcement function (Sec. 3.2.1) and then a simplified definition for safety properties (Sec. 3.2.2).

General Definition

The enforcement function can be described as a composition of functions, each performing the following steps: i) processing the input, ii) computing the delayed timed word satisfying the property, iii) and processing the output sequence. Moreover, the enforcement function describes how these functions are composed to transform an input sequence. We will then prove that it satisfies the physical, soundness, and transparency constraints.

Definition 8 (Enforcement function)

The enforcement function for a property ϕ is Eϕ :

(R ≥0 × Σ) * × R ≥0 → (R ≥0 × Σ) * defined as: Eϕ(σ, t) = obs Π 1 store(obs(σ, t)) , t .
where:

-store : (R ≥0 × Σ) * → (R ≥0 × Σ) * × (R ≥0 × Σ) * is defined as store( ) = ( , ) store(σ • (δ, a)) =    (σs • min lex,time K, ) if K = ∅, (σs, σc • (δ, a)) otherwise, with (σs, σc) = store(σ), K = κϕ(time(σ) + δ, σs, σc • (δ, a)),
κϕ(T, σs, σc) is the set defined as:

κϕ(T, σs, σc) def = {w ∈ (R ≥0 × Σ) * | w d σc ∧ |w| = |σc| ∧ σs • w |= ϕ ∧ delay(w(1)) ≥ T -time(σs))}, and
min lex,time stands for minimal timed word according to the lexical order among the timed words with minimal duration.

In the definition of Eϕ, obs(σ, t) is the prefix of the input that has been observed at time t, and thus can be processed by the enforcement function. The store function takes as input this observation, and computes a pair of timed words, whose first component extracted by Π 1 is processed by obs to produce the output.

The first element of the output of the store function is the transformation of a prefix of the observation for which delays have been computed (the property is satisfied by this prefix by appropriate delaying); the second element is the suffix of the observation for which delays still have to be computed. The store function is defined inductively: initially, for an empty observation, both elements are empty; if σ has been observed, store(σ) = (σs, σc), and a new event (δ, a) is observed, there are two possible cases, according to the vacuity of the set K = κϕ(time(σ) + δ, σs, σc • (δ, a)) (the set of candidate timed words appropriately delaying σc • (δ, a) and satisfying ϕ, see below):

-if K = ∅, among the set of timed words with minimal duration in K, the minimal timed word w.r.t the lexical order is appended to σs, and the second element is set to . -otherwise, (δ, a) is appended to σc and σs is not modified.

The function κϕ has three parameters: T (the duration of the current observation), σs, and σc. It computes the set of candidate timed words w "appropriately delaying" σc such that σs • w satisfies ϕ. The appropriate delaying is such that w and σc have identical actions, same length but delays of w are greater than or equal to those of σc. Moreover the delay of the first action in w should exceed the difference between the duration of the observation and the duration of σs. The reason for this constraint is that σs will be output entirely after a duration of time(σs), while the decision to output w is taken after T t.u., thus a smaller value for delay(w(1)) would cause this delay to be elapsed before the decision is taken. Notice that upon reading an input event (δ, a), in case if no appropriate delays exist, and correcting the sub-sequence σc • (δ, a) is impossible (when κϕ is empty), then the input event (δ, a) is appended to σc. If the sub-sequence σc • (δ, a) can be corrected, it is appended immediately to σs (with appropriate delays) without relying on events that will be read later. The adopted "policy" here is to correct the observation of the input sequence as soon as possible (see also Proposition 4 later). Consequently, the input sequence is treated as a series of sub-sequences, each sub-sequence allowing to satisfy the property.

Proposition 3 (Physicality, soundness, and transparency of enforcement functions) Given some property ϕ, its enforcement function Eϕ as per Definition 8 satisfies:

1. the physical constraints (Phy1) and (Phy2), 2. the soundness (Snd) and transparency (Tr) constraints, as per Definition 7.

In addition, the functional definition also ensures that each sub-sequence is output as soon as possible, as expressed by the following proposition: Proposition 4 (Optimality of enforcement functions) Given some property ϕ, its enforcement function Eϕ as per Definition 8 satisfies the following optimality constraint (Op):

∀σ ∈ (R ≥0 × Σ) * , ∀t ∈ R ≥0 : Eϕ(σ, t) = ∧ Eϕ(σ, t) |= ϕ =⇒ ∃wmx, w ∈ (R ≥0 × Σ) * : wmx = max ϕ ≺, (Eϕ(σ, t)) ∧Eϕ(σ, t) = wmx • w ∧ time(w) = min{time(w ) | delay(w (1)) ≥ time(σ [1•••|Eϕ(σ,t)|] ) -time(wmx) ∧ wmx • w |= ϕ ∧ Π Σ (w ) = Π Σ (w)}.
Intuition of optimality For any input σ, at any time t, if the output Eϕ(σ, t) is not , and satisfies ϕ, then the output is considered as two sub-sequences wmx, followed by w, such that wmx is the maximal strict prefix of Eϕ(σ, t), satisfying property ϕ and w is the remaining sub-sequence such that Eϕ(σ, t)) = wmx • w.

The last sub-sequence of the output which again makes the output to satisfy ϕ after wmx is w. The optimality constraint expresses that the sum of the delays (i.e., the time required to output) of w is minimal. The delay for the events in w should be chosen such that Eϕ(σ, t) = wmx • w satisfies ϕ and the transparency condition, and the delay of the first event is greater than the difference between the duration of the input sequence σ

[1•••|Eϕ(σ,t)|]
and the duration of wmx.

Notice that if time(σ

[1•••|Eϕ(σ,t)|]
) -time(wmx) is negative or null, then this means that the delay corresponding to some events in the sequence preceding w (which is wmx) are increased, providing sufficient amount of time to observe the last sub-sequence (which

is σ [|wmx|+1•••|wmx|+|w|] ) entirely. In case time(σ [1•••|Eϕ(σ,t)|] ) -time(wmx)
is positive, all events in wmx have been released as output before the last sub-sequence

σ [|wmx|+1•••|wmx|+|w|] is observed entirely as input. After releasing wmx, time(σ [1•••|Eϕ(σ,t)|]
) -time(wmx) time units have elapsed and thus the last sub-sequence w can be released as output only after a delay of time(σ

[1•••|Eϕ(σ,t)|] ) -time(wmx) time units.
Proof (of Propositions 3 and 4 -sketch only) The proofs are given in Appendices A.1 (for physical constraints), A.2 (for soundness and transparency), A.3 (for optimality), in p. 31, 32, 33, respectively. The proofs rely on an induction on the length of the input word σ. The induction step uses a case analysis, depending on whether the input is completely observed or not at time t, whether the input can be delayed into a correct output or not, and whether the memory content (computed by store) is completely dumped or not at time t.

The following example illustrates the notion of enforcement function.

Example 2 (Enforcement function) We now illustrate how Definition 8 is applied to enforce property ϕ 3 defined by the automaton depicted in Fig. 2c with Σ = {g, r}, and the input timed word σ = (3, g) • (10, r) • (3, g) • (5, g). Variable t describes global time. Figure 4 shows the evolution of obs, store, and Eϕ over time for the input σ. The resulting output is (13, g) • (15, r), which satisfies property ϕ 1 .

It is worth noticing that not all regular properties are enforceable, as illustrated by the following example.

Example 3 (Enforcement function: a non-enforceable property) Let us consider again property ϕ 4 , formalized by the TA in Fig. 2d, with Σ= {g, r}, and the input timed word σ = (3, r) • (4, g) • (2, r) • (6, g). Figure 5 shows the evolution of obs, store, and Eϕ. Variable t describes global time. The resulting output of the enforcement function is at any time instant.

obs(σ, t) = store ϕ (obs(σ, t)) = ( , ) E ϕ (σ, t) = obs( , t) obs(σ, t) = (3, g) store ϕ (obs(σ, t)) = ( , (3, g)) E ϕ (σ, t) = obs( , t) obs(σ, t) = (3, g) • (10, r) store ϕ (obs(σ, t)) = ((13, g) • (15, r), ) E ϕ (σ, t) = obs((13, g) • (15, r), t) obs(σ, t) = (3, g) • (10, r) • (3, g) store ϕ (obs(σ, t)) = ((13, g) • (15, r), (3, g)) E ϕ (σ, t) = obs((13, g) • (15, r), t) obs(σ, t) = (3, g) • (10, r) • (3, g) • (5, g) store ϕ (obs(σ, t)) = ((13, g) • (15, r), (3, g) • (5, g)) E ϕ (σ, t) = obs((13, g) • (15, r), t) t ∈ [0, 3[ t ∈ [3, 13[ t ∈ [13, 16[ t ∈ [16, 21[ t ∈ [21, ∞[
obs(σ, t) = store ϕ (obs(σ, t)) = ( , ) E ϕ (σ, t) = obs( , t) obs(σ, t) = (3, r) store ϕ (obs(σ, t)) = ( , (3, r)) E ϕ (σ, t) = obs( , t) obs(σ, t) = (3, r) • (4, g) store ϕ (obs(σ, t)) = ( , (3, r) • (4, g)) E ϕ (σ, t) = obs( , t) obs(σ, t) = (3, r) • (4, g) • (2, r) store ϕ (obs(σ, t)) = ( , (3, r) • (4, g) • (2, r)) E ϕ (σ, t) = obs( , t) obs(σ, t) = (3, r) • (4, g) • (2, r) • (6, g) store ϕ (obs(σ, t)) = ( , (3, r) • (4, g) • (2, r) • (6, g)) E ϕ (σ, t) = obs( , t) t ∈ [0, 3[ t ∈ [3, 7[ t ∈ [7, 9[ t ∈ [9, 15[ t ∈ [15, ∞[
Remark 3 (Non-enforceable properties) From Example 3, notice that the output of the enforcement function is , though the input sequence itself satisfies the property. The monitor observes action r followed by action g only at t = 7. Hence, the delay associated with the first action in output should be at least 7 t.u., but increasing the delay associated with the first action to 7, would falsify the guard on transition between l 0 to l 1 , which is a possible move upon the first event req, and there is no transition with a reset of clock x before.

It can be noticed that guards with <, ≤, and = impose urgency on releasing an event as output at or before some time. For some properties, some input sequences that can be delayed to satisfy ϕ cannot be corrected by enforcement, because the delay of the first event of each sub-sequence may be increased, which may falsify a guard with <, ≤, =. However, even for such properties, the enforcement function will never produce incorrect outputs. Moreover, note that the notion of non-enforceability exhibited here does not stem from the fact that we focus on enforcement mechanisms that act as delayers. Indeed, even if our enforcement mechanisms were able to reduce delays between events (by for instance releasing g immediately after r), the property would remain non-enforceable because of the guard "x ≤ 5" on the transition between locations l 0 and l 1 .

Remark 4 (Alternative enforcement strategies) The optimality constraint presented in Proposition 4 allows only to augment delays of events. For each event, a delay greater than or equal to the actual delay is chosen. This condition can be modified or relaxed according to our requirements. This condition can be easily adapted to a given time bound in R ≥0 . It may also be possible to shorten the delay of some events (as long as the duration of the output is greater than the input, i.e. when it satisfies Phy2). Additionally, processing input and output actions is assumed to be done in zero time. Some delay (either fixed or depending on additional parameters) can be considered for this action by modifying the store function, and adding this constraint in the definition of κϕ. Such modification would reduce the set of enforceable properties.

Remark 5 (Elimination of some acceptable behaviors by the enforcement function) As we saw earlier in Remark 3, some input sequences that can be delayed to satisfy ϕ cannot be accepted (and released as output) by the enforcement function. This behavior of the enforcement function stems from the following facts:

-At anytime, decision is taken based on the input events received until that time, and the enforcer has no information regarding the events that it will receive in the future. -Moreover, we defined optimality in such a way that, the decision about releasing events is taken as soon as possible (when a mechanism knows that there is a possibility to correct, it does not wait for any further input events).

Note, this is also the case for control mechanisms in supervisory control theory for discrete event systems.

Simplified Functional Definitions

The functional definitions for enforcement in the case of safety or co-safety properties can be simplified. As an example, we briefly explain how the functional definition can be simplified for safety properties.

Simplified functional definition for safety properties. For safety properties, the store function can be simplified: the output is a timed word instead of a pair of timed words (store sa ϕ : (R ≥0 × Σ) * → (R ≥0 × Σ) * ). In fact for a safety property, the delay of each input event, if there exists one, can be computed immediately. Thus the second element of the store output pair (which stores events with undetermined delays) is unnecessary. The store function for safety properties can be defined as follows:

store sa ϕ ( ) = store sa ϕ (σ • (δ, a)) = store sa ϕ (σ) • (min(K), a) if K = ∅, store sa ϕ (σ) otherwise,
where

K def = {δ ∈ R ≥0 | δ ≥ δ∧store sa ϕ (σ)•(δ , a) d σ•(δ, a)∧store sa ϕ (σ)•(δ , a)
|= ϕ}. K is the set of delays δ that can be associated to a such that the extension store sa ϕ (σ) • (δ , a) of the previous store sa ϕ (σ) delays σ • (δ, a) and still satisfies property ϕ. It depends on ϕ, σ (more precisely store sa ϕ (σ)), and (δ, a).

Remark 6 For the particular case of safety properties, Propositions 3 and 4 also hold when using the simplified functional definition (using the store sa ϕ function). Moreover, with the alternative functional definition for safety properties using function store sa ϕ , the optimality constraint in Proposition 4 which the enforcement function satisfies can be simplified and defined alternatively as follows.

Simplified optimality constraint of an enforcement function for safety properties. If Eϕ is sound, transparent, and satisfies the physical constraints (Phy1) and (Phy2), Eϕ is said to be optimal if the following constraint holds:

∀σ ∈ (R ≥0 × Σ) * , ∀t ∈ R ≥0 : |Eϕ(σ, t)| = max |o | | o d obs(σ, t) ∧ o |= ϕ ∩ ( Eϕ(σ, t) • (R ≥0 × Σ) * ) (Op-saf)
where Eϕ(σ, t)

def = max {Eϕ(σ, t ) | t < t}.
The optimality constraint (Op-saf) expresses that at any time instant t, the output sequence Eϕ(σ, t) should be the longest correct timed word delaying the input sequence obs(σ, t) that extends Eϕ(σ, t), the maximal output sequence strictly before t. Notice that the term (R ≥0 × Σ) * takes into account the fact that several timed actions may be output at time t.

Enforcement Monitor

In what follows, we consider a property ϕ defined by a TA Aϕ whose semantics is a transition system

[[Aϕ]] = (Q, q 0 , Γ, →, F G ).
An enforcement function Eϕ for ϕ is implemented by an enforcement monitor (EM), defined as a transition system E. An EM is an operational view of the enforcement function. It is equipped with a memory and a set of enforcement operations used to store and dump some timed events to and from the memory, respectively. The memory of an EM consists of two queues, each containing a timed word, one storing the received actions (with increased delays) which are corrected and can be released as output. The other queue stores the actions that are read by the EM, but are yet to be corrected (and cannot be released as output). In addition, an EM also keeps track of the state of the underlying TA, and clock values used to count time between input events and between output events.

Before presenting the definition of enforcement monitor, we introduce update as a func-

tion from Q × (R ≥0 × Σ) + × R ≥0 to (R ≥0 × Σ) + × B.
The update function takes as input a triple (q, σc, m t ) where q ∈ Q is the (current) state of [[Aϕ]], σc ∈ (R ≥0 × Σ) + is a non-empty timed word, and m t ∈ R ≥0 is the difference between the duration of the input sequence observed minus the duration of the corrected sequence, and returns a timed word of length |σc| and a Boolean as output.

update(q, σc, m t ) def =    σc, ff if Λ(σc, m t , q) = ∅, σ c , tt otherwise;
where

σ c = min lex,time Λ(σc, m t , q) with Λ : (R ≥0 × Σ) + × R ≥0 × Q → 2 (R ≥0 ×Σ) * defined as: Λ(σc, m t , q) = {w ∈ (R ≥0 × Σ) + | w d σc ∧ |w| = |σc| ∧ delay(w(1)) ≥ m t ∧q w → F G }.
Λ(σc, m t , q) is the set of timed words w of length |σc| with same actions as σc, each delay in the sequence is equal to or greater than the delay at the corresponding index in the provided input sequence σc, and the first delay in w should be greater than or equal to m t , and an accepting state is reachable from state q upon sequence w.

-The first case applies when there are no good delays such that an accepting state is reachable from the state q upon with a sequence delaying σc (Λ(σc, m t , q) = ∅). In this case, the update function returns the same timed word σc (which is provided as input), and a Boolean value ff, indicating that no accepting state is reachable. -The second case applies when there are good delays and an accepting state in q 1 ∈ Q F is reachable from q upon a sequence delayed from σc. In this case, the update function returns a timed word of minimal duration belonging to Λ(σc, m t , q), chosen according to the lexical order; and a Boolean value tt, indicating that an accepting state is reachable.

Definition 9 (Enforcement Monitor) An enforcement monitor E for ϕ is a transition system

(C E , c E 0 , Γ E , → E ) s.t.: -C E = (R ≥0 × Σ) * × (R ≥0 × Σ) * × R ≥0 × R ≥0 × R ≥0 × Q is the set of configurations, -c E 0 = ε, ε, 0, 0, 0, q 0 ∈ C E is the initial configuration, -Γ E = (R ≥0 ×Σ)∪{ } ×Op× (R ≥0 ×Σ)∪{ } is the alphabet, which is composed of
triples, comprised of an optional input event, an operation, and an optional output event, where the set of possible operations is

Op = {store-ϕ(•), store-ϕ(•), dump(•), idle(•)}; -→ E ⊆ C E × Γ E × C E
is the transition relation defined as the smallest relation obtained by the following rules applied with the priority order below: -1. store-ϕ:

(σs, σc, δ, d, m t , q) (δ,a)/store-ϕ(δ,a)/ → E (σs, σc • (δ, a), 0, d, m t , q), if Π 2 (update(q, σc • (δ, a), m t + δ)) = ff, where: -m t = m t + δ -2. store-ϕ: (σs, σc, δ, d, m t , q) (δ,a)/store-ϕ(δ,a)/ → E (σs • σ c , , 0, d, m t , q ), if update(q, σc • (δ, a), m t + δ)) = (σ c , tt), where: -m t = m t + δ -time(σ c ) -q is defined as q σ c → q -3. dump:
((δ, a) • σs, σc, s, δ, m t , q) / dump(δ,a)/(δ,a) → E (σs, σc, s, 0, m t , q) -4. idle:

(σs, σc, s, d, m t , q)

/ idle(δ)/ → E (σs, σc, s + δ, d + δ, m t , q).
A configuration (σs, σc, s, d, m t , q) of the EM consists of the current stored sequence (i.e., the memory content) σs, and σc. The sequence that is corrected and can be released as output is denoted by σs. The sequence σc is sort of an internal memory for the store function: this is the input sequence read by the EM, but yet to be corrected. The configuration also contains two clock values s and d indicating respectively the time elapsed since the last store and dump operations, and one more counter m t indicating the difference between the duration of the observed input sequence and the duration of the corrected sequence. q is the current state of [[Aϕ]] reached after processing the sequence already released followed by the timed word in memory σs.

Semantic rules can be understood as follows:

-Upon reception of an event (δ, a), one of the following store rules is executed.

-The store-ϕ rule is executed if the update function returns ff (indicating that σc • (δ, a) cannot be corrected). The clock s is reset to 0, and the event (δ, a) is appended to the internal memory σc. The delay corresponding to the input event δ is added to m t . -The store-ϕ rule is executed if the update function returns tt, indicating that ϕ can be satisfied for the sequence already released as output, followed by the sequence in σs, followed by σc • (δ, a) with possibly increased delays. When executing this rule, s is reset to 0, and the timed word σ c returned by the update function is appended to the content of the output memory σs. The delay of the input event δ is added to m t , and the duration of the corrected sub-sequence returned by the update function, time(σ c ), is subtracted from m t . -The dump rule is executed if the time elapsed since the last dump operation d, is equal to the delay corresponding to the first event of the timed word σs in the memory. The event (δ, a) is released as output and removed from σs, and the clock d is reset to 0. -The idle rule adds the time elapsed δ to the current values of s and d when neither the store nor the dump rule applies.

Example 4 (Execution of an enforcement monitor) We now illustrate how the rules of Definition 9 are applied to enforce property ϕ 3 , defined by the automaton depicted in Fig. 2c.

Let us consider the input timed word σ = (3, g) • (10, r) • (3, g) • (5, g). Figure 6 shows how semantic rules are applied, and the evolution of the configurations of the enforcement monitor. In a configuration, the input (resp. output) is on the right (resp. left). Variable t describes global time. The resulting output is (13, g) • (15, r), which satisfies property ϕ 3 .

From t = 28, only the idle rule can be applied.

Remark 7 (Simplified definitions of enforcement monitor)

To synthesize an EM for a safety or co-safety property, one can use simplified definitions. For example, for a safety property, only one timed word is needed in the configuration. Indeed, recall that σc is a sort of internal memory used to store the input events used when it may be possible to reach an accepting state if more events are observed in the future. Since a safety property is prefix-closed, upon an event that cannot be delayed to keep satisfying the property, no future extension can. Hence, σc is not necessary for safety properties. Therefore, some simplifications, that may lead to performance improvements, are possible.

Relating Enforcement Functions and Enforcement Monitors

We present how the definitions of enforcement function and enforcement monitor can be related: given a property ϕ, any input sequence σ, at any time instant t, the output of the associated enforcement function and the output-behavior of the associated enforcement monitor are equal. We first describe how an enforcement monitor reacts to an input sequence. In the remainder of this section, we consider an enforcement monitor E = (C E , c E 0 , Γ E , →E). Enforcement monitors, as defined in Section 3.3, are deterministic. By determinism, we mean that the observable behavior of our enforcement monitors, i.e., given an input sequence the observable output sequence is unique. Moreover, given σ ∈ (R ≥0 × Σ) * and t ∈ R ≥0 , how an enforcement monitor reads σ until time t is unique: it goes through a unique sequence of configurations. However, given an input sequence σ and a time instant t, because /( , , 0, 0, 0, (l 0 , 0))/( 3 of 's in the input alphabet there is possibly an infinite set of corresponding sequences over the input-operation-output alphabet (as in Definition 9). All these sequences are equivalent: they involve the same configurations for the enforcement monitor and the same output sequence. Consequently, the rules of the transition relations are ordered in such a way that reading will always be the transition with least priority. As a consequence given an input sequence reading (and doing other operations such as outputting some event) will always be possible when the monitor cannot read an input. This constraint is consistent with our hypothesis stating that enforcement monitors execute infinitely faster than their environment.

More formally, let us define E ioo (σ, t) ∈ (Γ E ) * to be the unique sequence over the alphabet of actions (triples comprised of an optional input event, an operation, and an optional output event) that is "triggered" when the enforcement monitor reads σ until time t.

Definition 10 (Input-Operation-Output sequence) Given an input sequence σ ∈ (R ≥0 × Σ) * and some time instant t ∈ R ≥0 , we define the input-operation-output sequence denoted as E ioo (σ, t) and which triggered when an enforcement monitor of initial configuration c E 0 reads σ until time t. E ioo (σ, t) is defined as the unique sequence of (Γ E ) * such that:

∃c ∈ C E : c E 0 Eioo(σ,t) → * E c ∧ Π 1 (E ioo (σ, t)) = obs(σ, t) ∧ timeop(Π 2 (E ioo (σ, t))) = t ∧ c ∈ C E , ∃e ∈ (R ≥0 × Σ) : c ( ,dump(e),e) → c ,
where the timeop function indicates the duration of a sequence of enforcement operations and says that only the idle enforcement operation consumes time. Formally:

timeop(op • ops) = d + timeop(ops) if ∃d ∈ R ≥0 : op = idle(d), timeop(ops) otherwise; timeop( ) = 0.
The input timed word corresponding to obs(σ, t) at any time t is the concatenation of all the input events read/consumed by the enforcement monitor over various steps. Observe that because of the assumptions on Γ E , only the idle rule applies to the configuration c: the dump rule does not apply by definition of E ioo (σ, t) and none of the store rules applies because Π 1 (E ioo (σ, t)) = obs(σ, t).

Relating enforcement functions and enforcement monitors. Now, we can relate the enforcement function and the enforcement monitor, for a property ϕ. Seen from the outside, an enforcement monitor E behaves as a device reading and producing timed words. Overloading notations, we can characterize this input/output behavior as a function

E : (R ≥0 ×Σ) * × R ≥0 → (R ≥0 × Σ) * defined as: ∀σ ∈ (R ≥0 × Σ) * , ∀t ∈ R ≥0 : E(σ, t) = Π 3 E ioo (σ, t) .
The corresponding output timed word E(σ, t) at any time t is the concatenation of all the output events produced by the enforcement monitor over various steps of the enforcement monitor (erasing 's). As before, the 's output by the store operation are erased. In the following, we do not make the distinction between an enforcement monitor and the function that characterizes its behavior.

Finally, we are able to relate enforcement functions, and the functions derived from an enforcement monitor. For this purpose, we define an implementation relation between enforcement monitors and enforcement functions as follows.

Definition 11 (Implementation relation between enforcement functions and enforcement monitors) Given an enforcement function Eϕ (as per Definition 6) and an enforcement monitor (as per Definition 9) whose behavior is characterized by a function E, we say that E implements Eϕ iff:

∀σ ∈ (R ≥0 × Σ) * , ∀t ∈ R ≥0 : Eϕ(σ, t) = E(σ, t).
Proposition 5 (Relation between enforcement function and enforcement monitor) Given a property ϕ, its enforcement function Eϕ (as per Definition 8), and its enforcement monitor E (as per Definition 9), E implements Eϕ in the sense of Definition 11.

Proof (of Proposition 5 -sketch only)

The proof is given in Appendix A, p. 37. The proof is done by induction on the length of the input sequence and uses a similar case analysis as the proof of Proposition A.2. The proof also uses several intermediate lemmas that characterize some special configurations (e.g., value of the store and dump variables, memory content) of an enforcement monitor at some time instants.

Implementation of Enforcement Monitors

Let us now see the algorithms, which are a straightforward translation of the EM semantics, showing how enforcement monitors can be implemented. The implementation of an EM consists of two processes running concurrently (Store and Dump) as shown in Figure 7, and a memory. The Store process models the store rules. The memory contains the timed word σs: the corrected sequence that can be released as output. The memory σs is realized as a queue, shared by the Store and Dump processes, where the Store process adds events which are processed and corrected to this queue. The Dump process reads events stored in the memory σs and releases them as output after the required amount of time. The Store process also makes use of another internal buffer σc (not shared with any other process), to store the events which are read, but cannot be corrected (to satisfy the property). In the algorithms the await primitive is used to wait for a trigger event from another process or to wait until some condition becomes true. The wait primitive is used by a process to wait for a certain amount of time, that is determined by the process itself.

Enforcement Monitor

Dump Process

Store Process

Memory (σs) σc Eϕ(σ, t) σ, t Fig. 7 Realizing an EM

The StoreProcess algorithm (see Algorithm 1) is an infinite loop that scrutinizes the system for input events. In the algorithm, (l, ν) represents the state of the automaton defining the property, where l represents the location and ν is the current clock valuation. It is initialized to (l 0 , [X ← 0]). The variable m t is used to keep track of the difference between the duration of the input sequence read (the sequence which is already corrected followed by the sequence in σc), and the duration of the corrected sequence. The update function takes the events stored in the internal memory of the store process σc, the current state, and m t , and returns a timed word of same length as σc and a Boolean indicating whether an accepting state is reachable from the current state upon the timed word it returns as a result. The function post takes a state of the automaton defining the property (l, ν), a timed word, and computes the state reached by this automaton.

The algorithm proceeds as follows. The StoreProcess initially waits for an input event. A received event is appended to the internal buffer σc, with the corresponding delay δ, and this delay δ is added to m t . Then the update function is invoked providing the events stored in σc as input. If the update function indicates that there is a path leading to an accepting state, (i.e., if isPath = tt), then the timed word σ c returned by the update function, is appended to the shared memory σs (since it now corrected with respect to the property, and can be released as output). Then, the duration of σ c is subtracted from m t . Before proceeding to the next iteration, the state of the automaton (l, ν) is updated, and the internal memory σc is cleared.

The DumpProcess algorithm (see Algorithm 2) is an infinite loop that scrutinizes the memory and proceeds as follows: Initially, the clock d is set to 0. If the memory is empty (σs = ), the DumpProcess waits until a new element (δ, a) is stored in the memory. Else (the memory is not empty), it proceeds with the first element in the memory. Using the dequeue operation, the first element stored in the memory is removed, and is stored as

Algorithm 1 StoreProcess (l, ν) ← (l 0 , [X ← 0]) (σs, σc) ← ( , ) mt ← 0 while tt do (δ, a) ← await(event) σc ← σc • (δ, a) mt ← mt + δ (σ c , isPath) ← update(l, ν, σc, mt) if isPath = tt then mt ← mt -time(σ c ) σs ← σs • σ c (l, ν) ← post(l, ν, σ c ) σc ← end if end while Algorithm 2 DumpProcess d ← 0 while tt do await(σs = ) (δ, a) ← dequeue (σs) wait(δ -d) dump (a) d ← 0 end while
(δ, a). Meanwhile, d keeps track of the time elapsed since the last dump operation. The DumpProcess waits for (δ-d) time units before performing the dump(a) operation, releasing the action a as output (which amounts to appending (δ, a) to the output of the enforcement monitor). Finally, the clock d is reset to 0 before the next iteration starts.

Remark 8 (Using non-deterministic TAs to define properties) In this paper, the presentation considers only deterministic TAs. Extending the results to non-deterministic TAs comes directly from the policy used to choose a unique solution to define the update function (which computes the correct and optimal delays). The update function first computes all accepting paths from the current state, for the given input sub-sequence. And from this set of all accepting paths, a unique solution with minimal duration is chosen using the lexical order. Thus, note that the same mechanisms and algorithms remain valid (without requiring any change) to also enforce properties defined with non-deterministic TAs.

Remark 9 (Simplified algorithms) For safety and co-safety properties, if we want to implement monitors following the simplified functional and enforcement monitor definitions, the algorithm for the StoreProcess can also be simplified. In particular, in the algorithm for safety properties, the content of the memory can be maintained by a single sequence of events instead of a tuple. Also, in case of safety properties, the update function is always invoked with a single event as input, instead of a sequence of events. The simplified algorithms for safety and co-safety properties are described in detail in [START_REF] Pinisetty | Runtime enforcement of timed properties[END_REF].

Remark 10 (Enforcing several properties) Earlier in this section, we described how any regular property can be enforced. When a boolean combination of properties has to be enforced on a system, we can combine the properties in a single one and synthesize one enforcement monitor for the resulting property. Definition 4 in Section 2 describes how two properties defined by TAs can be combined using Boolean operations (e.g., union, intersection and negation).

Implementation and Evaluation

We implemented the algorithms in Sec. 3.5 and developed an experimentation framework called TIPEX: (TImed Properties Enforcement during eXecution) in order to:

1. validate through experiments the architecture and feasibility of enforcement monitoring, and 2. measure and analyze the performance of the update function of the StoreProcess in the case of safety and co-safety properties.

From [START_REF] Pinisetty | Runtime enforcement of timed properties[END_REF], we completely re-implemented the enforcement monitors. Still following the algorithms proposed in [START_REF] Pinisetty | Runtime enforcement of timed properties[END_REF], TIPEX is more independent and offers better performance. It is now completely independent from UPPAAL at runtime. Moreover, TIPEX does not invoke UPPAAL to realize update anymore, and some other redundancies, such as updating the UPPAAL model file after each event, are also eliminated.

In this paper, we focus on evaluating the performance using some safety and co-safety properties. In Sec. 3, we described how the definitions of enforcement mechanisms can be simplified if we know that the property is safety (or co-safety). Thus, instead of using the algorithms proposed for regular properties in Sec. 3.5, TIPEX is implemented using the algorithms based on the simplified definitions for safety and co-safety properties described in [START_REF] Pinisetty | Runtime enforcement of timed properties[END_REF]. Extending TIPEX for regular properties based on the algorithms proposed in this paper, and evaluation using some regular properties which are neither safety nor co-safety, is ongoing.

We focus on benchmarking the update function of the StoreProcess for safety and cosafety properties proposed in [START_REF] Pinisetty | Runtime enforcement of timed properties[END_REF], which are the simplified versions of the general StoreProcess described in section 3.5. Indeed, examining the algorithms, the steps in the algorithm of the DumpProcess of monitors are algorithmically simple and lightweight from a computational point of view. Regarding the StoreProcess function for safety and co-safety properties, their most computationally intensive step is their call to their update function.

Experimental framework. Let us briefly look into the experimental framework, which is depicted in Fig. 8. The Main module uses the module Trace Generator that provides a set of input traces, to test the Store module. The Trace Generator module takes as input the alphabet of actions, the range of possible delays between actions, the desired number of traces, and the increment in length per trace. For example if the number of traces in 5, and increment in length per trace is 100 then 5 traces will be generated, where the first trace is of length 100 and the second trace of length 200 and so on. It returns a set of traces. For each event, the Trace Generator picks an action (from the set of possible actions), and a delay (from the set of possible delays) randomly using methods from the Python random module.

The Store module takes as input a property and one trace, and returns the total execution of the update function to process the given input trace. The TA modeling the property is a UPPAAL [START_REF] Larsen | UPPAAL in a nutshell[END_REF] model written in XML. The Store module uses the pyuppaal library to parse the UPPAAL model (input property), and the UPPAAL DBM library to implement the update function. 4 More details about the implementation of the Store module for safety and co-safety properties are in Appendix B. The UPPAAL model also contains another automaton representing the sequence of events received by the enforcement monitor. The Main Test Method sends the sequence to the Store module (using the property), and keeps track of the result returned by the Store module for each trace.

Experiments were conducted on an Intel Core i7-2720QM at 2.20GHz CPU, with 4 GB RAM, and running on Ubuntu 12.04 LTS. The reported numbers are mean values over 10 runs and are represented in seconds. We have chosen to compute the average values over 10 runs because, for all metrics, with 95% confidence, the measurement error was less than 1%. For example, referring to Table 1, for the safety property ϕ 1.1 s , the mean value of the total execution time of the update function is 8.6306 seconds, and the error is 0.018 seconds. Thus with 95% confidence, the execution time of update for input trace of length 10000 lies within the interval [8.6126, 8.6486] (seconds). For the average time per call, as shown in the table, ϕ 1.1 s , the mean value is 0.863 milli-seconds, and the error is 0.005 milliseconds. Thus, with 95% confidence, the average time per call to update, for input trace of length 10000 lies within the interval [0.858, 0.868] (milliseconds).

Performance evaluation of the update function for safety properties

We describe the properties used in our experiments and discuss the results of the performance analysis. The considered safety properties follow different patterns [START_REF] Gruhn | Patterns for timed property specifications[END_REF]. Property ϕ 1 s belongs to the absence pattern. It expresses that "There cannot be n or more aactions in every k time units", where n is a parameter of the pattern. Following this pattern, the considered properties are ϕ 1, as expected for safety properties, we can observe that the time taken per call to update is independent on the length of the trace. This behavior is as expected: since we update the state of the TA after each event, and after receiving a new event, we explore the possible transitions leading to a good state from the current state. Moreover, from the curves shown in Fig. 9, notice that, for a given trace length, the execution time of update is similar for the two patterns and their variants in size. We describe the properties used in our experiments and discuss the results of the performance analysis. The considered co-safety properties follow different patterns [START_REF] Gruhn | Patterns for timed property specifications[END_REF].

Property ϕ 1 cs belongs to the existence pattern [START_REF] Gruhn | Patterns for timed property specifications[END_REF]. It expresses that "There should be n ractions, which should be immediately followed by a g-action with a delay of at least k time units". Following this pattern, the considered properties are ϕ 1.1 cs and ϕ 1.2 cs each varying in the value of n: n = 1 for ϕ 1.1 cs , and n = 5 for ϕ 1.2 cs .

Results and analysis. Results of the performance analysis of our running example properties are presented in Table 2. Entry t update indicates the execution time of function update. Entry t avg is the average time per call, and the entry t last is the execution time of update upon the last event. Note that the execution on the last event is the most time consuming. The considered input traces are generated in such a way that an accepting state is reachable only upon the last event. From the results presented in Table 2, notice that t last and t avg increase with |tr|. This behavior is as expected for a co-safety property because the update function starts the computation from the initial state for a given input trace. This behavior is also clearly shown by the curves in Fig. 10, showing the total time taken by the update function versus the length of the input trace. Moreover, notice that, for a given trace length, the execution time of update is similar for the two properties of the same pattern varying in size.

Remark 11

In case of a co-safety property, the monitor starts to output events only after reading an input sequence which can satisfy the property (after the optimal delays are computed for the input sequence). Once an accepting state is reached, then it is not necessary to invoke the update and to correct the delays anymore.

Discussion

On precision. In theory, the delays between actions and the optimal delay computed by the update function are real numbers. In the implementation, in order to compute optimal delay, we need to set precision. We use UPPAAL [START_REF] Larsen | UPPAAL in a nutshell[END_REF] to model the input TA, and some UPPAAL libraries to realize the algorithms. In UPPAAL, only integers can be used to compare the values of clocks in the guards. But, in practice, we may have to use real-numbers to express requirements and timing constraints. This issue can be handled by setting the precision of real-numbers, and representing values on guards with equivalent integers. For example, if we set the precision with four digits after the decimal point, 0.0024 can be represented as 24, and 5.0012 can be represented as 50012. Note that having a large integer value on a guard such as in x > 50000 is not an issue with region and zone computations, as computation is done on-the-fly. After each event, we check for possible paths from the current state.

On performance and overhead. Assessing the performance of runtime enforcement monitors is paramount in a timed context as. Using the experimental results, one can determine the guards and the properties for which the assumptions stated in the introduction hold. Regarding safety properties, one can see that, on the used experimental setup, the computation time of the update function is below 1ms. By taking guards with constraints using integers above 0.1s, one can see that the computation time can be negligible in some sense as the impact on the guard is below 1%, and makes the overhead of enforcement monitoring acceptable.

Related Work

Several runtime verification and enforcement approaches are related to the one proposed in this paper. We propose a comparison with approaches for the runtime enforcement of untimed properties (Sec. 5.1), for the runtime verification of timed properties (Sec. 5.2), and runtime enforcement of timed properties (Sec. 5.3)

Runtime Enforcement of Untimed Properties

Most of the work in runtime enforcement was dedicated to untimed properties (see [START_REF] Falcone | You should better enforce than verify[END_REF] for a short overview). Schneider introduced security automata as the first runtime mechanism for enforcing safety properties [START_REF] Schneider | Enforceable security policies[END_REF]. Then the set of enforceable properties was later refined by Schneider, Hamlen, and Morrisett by showing that security automata were actually restrained by the computational limits exhibited by Viswanathan and Kim [START_REF] Viswanathan | Foundations for the run-time monitoring of reactive systems -Fundamentals of the MaC language[END_REF]: the set of co-recursively enumerable safety properties is a strict upper limit of the power of (execution) enforcement monitors defined as security automata. Ligatti et al. [START_REF] Ligatti | Run-time enforcement of nonsafety policies[END_REF] later introduced edit-automata as enforcement monitors. Edit-automata can either insert a new action by replacing the current input, or suppress it. The set of properties enforced by edit-automata is called the set of infinite renewal properties: it is a super-set of safety properties and contains some liveness properties (but not all). Similar to edit-automata are generic enforcement monitors [START_REF] Falcone | Runtime enforcement monitors: composition, synthesis, and enforcement abilities[END_REF] are able to enforce the set of (untimed) response regular properties in the safety-progress classification. Moreover, some variants of edit-automata differ in how they ensure the transparency constraints (see e.g., [START_REF] Bielova | Do you really mean what you actually enforced? -edited automata revisited[END_REF]).

Runtime Verification of Timed Properties

Several approaches have been proposed for the runtime verification of timed properties. We shall categorize them into i) rather theoretical efforts aiming at synthesizing monitors (Sec. 5.2.1), and ii) tools for runtime monitoring of timed properties (Sec. 5.2.2).

Synthesis of Timed Automata from Timed Logical Formalisms

Bauer et al. propose an approach to runtime verify timed-bounded properties expressed in a variant of Timed Linear Temporal Logic (TLTL) [START_REF] Bauer | Runtime verification for LTL and TLTL[END_REF]. Contrarily to TLTL, the considered logic, TLTL 3 , processes finite timed words and the truth-values of this logic are suitable for monitoring. After reading some timed word u, the monitor synthesized for a TLTL 3 formula ϕ states the verdict (resp. ⊥) when there is no infinite timed continuation w such that u • w satisfy (resp. does not satisfy) ϕ. Another variant of LTL in a timed context is Metric Temporal Logic (MTL), a dense extension of LTL. Nickovic et al. [START_REF] Maler | From MITL to timed automata[END_REF][START_REF] Nickovic | From MTL to deterministic timed automata[END_REF] propose a translation of MTL to timed automata. The translation is defined under the bounded variability assumption stating that, in a finite interval, a bounded number of events can arrive to the monitor. Still for MTL, Thati et al. propose an online monitoring algorithm which works by rewriting of the monitored formula and study its complexity [START_REF] Thati | Monitoring algorithms for metric temporal logic specifications[END_REF]. Basin et al. propose an improvement of the aforementioned approach with a better complexity but considering only the past fragment of MTL [START_REF] Basin | Algorithms for monitoring real-time properties[END_REF].

Runtime enforcement of timed properties as presented in this paper is compatible with the previously-described approaches. These approaches synthesize audtomata-based decision procedures for logical formalisms. Decision procedures synthesized for regular properties can be used as input to our framework.

Tools for Runtime Monitoring of Timed Properties

The Analog Monitoring Tool [START_REF] Nickovic | AMT: a property-based monitoring tool for analog systems[END_REF] is a tool for monitoring specifications over continuous signals. The input logic of AMT is STL/PSL where continuous signals are abstracted into propositions and operations are defined over signals. Input signal traces can be monitored in an offline or incremental fashion (i.e., online monitoring with periodic trace accumulation).

RT-MaC [START_REF] Sammapun | RT-MaC: Runtime monitoring and checking of quantitative and probabilistic properties[END_REF] is a tool for verifying timed properties at runtime. RT-MaC allows to verify timeliness and reliability correctness. Using the time-bound temporal operators provided by the tool, one can specify a deadline after which a property must hold.

LARVA [START_REF] Colombo | Dynamic event-based runtime monitoring of real-time and contextual properties[END_REF][START_REF] Colombo | LARVA -safer monitoring of real-time Java programs (tool paper)[END_REF] takes as input properties expressed in several notations, e.g., Lustre, duration calculus. Properties are translated to DATE (Dynamic Automata with Timers and Events) which basically resemble timed automata with stop watches but also feature resets, pauses, and can be composed into networks. Transitions are augmented with code that modify the internal system state. DATE target only safety properties. In addition, LARVA is able to compute an upper-bound on the overhead induced on the target system. The authors also identify a subset of the duration calculus, called counter-examples traces, where properties are insensitive to monitoring [START_REF] Colombo | Safe runtime verification of real-time properties[END_REF].

Our monitors not only differ by their objectives but also by how they are interfaced with the system. We propose a less restrictive framework where monitors asynchronously read the outputs of the target system. We do not assume our monitors to be able to modify the internal state of the target program. The objective of our monitors is rather to correct the timed sequence of output events before this sequence is released to the environment (i.e., outside the system augmented with a monitor).

Runtime Enforcement of Timed Properties

Matteucci inspires from partial-model checking techniques to synthesize controller operations to enforce safety and information-flow properties using process-algebra [START_REF] Matteucci | Automated synthesis of enforcing mechanisms for security properties in a timed setting[END_REF]. Monitors are close to Schneider's security automata [START_REF] Schneider | Enforceable security policies[END_REF]. The approach targets discrete-time properties and systems are modeled as timed processes expressed in CCS. Compared to our approach, the description of enforcement mechanisms remains abstract, directly restricts the monitored system, and no description of monitor implementation is proposed. Besides, in a general study, Rinard discusses monitoring and enforcement strategies for real-time systems [START_REF] Rinard | Acceptability-oriented computing[END_REF], and mentions the fact that enforcement mechanisms could delay input individual events in an input stream when they arrive too early w.r.t. the constraints of the system. In the same way, we consider in our work that an enforcer is time retardant. However, the work in [START_REF] Rinard | Acceptability-oriented computing[END_REF] remains at a high-level of abstraction and does not propose any detailed description of enforcement mechanisms.

More recently, Basin et al. [START_REF] Basin | Enforceable security policies revisited[END_REF] proposed a general approach related to enforcement of security policies with controllable and uncontrollable events, investigating enforceability (with complexity results), and how to synthesize enforcement mechanisms for several specification formalisms (automata-based or logic-based). A monitor observes the system and terminates it to prevent violations. Timed properties described in MLTL logic are handled in this work. Discrete time is considered, clock ticks are used to determine the enforceability of an MLTL formula. In our approach, we consider dense time, using the expressiveness of timed automata and efficiency of UPPAAL. Moreover, our enforcement mechanisms may modify the execution of the observed system, and termination is decided if correcting the execution by delaying is not possible.

Conclusion and Future Work

Conclusion. This paper presents a general enforcement monitoring framework for systems with (dense) timing requirements. We showed how to synthesize enforcement mechanisms for any regular timed property (modeled with a timed automaton). We propose adapted notions of enforcement mechanisms that delay input actions in order to satisfy the required property. Enforcement mechanisms are described at several levels of abstraction (enforcement function, monitor, and algorithm), thus facilitating the design and implementation of such mechanisms. We describe how to realize the enforcement monitor using concurrent processes. We propose a prototype implementation and our experiments demonstrate the feasibility of enforcement monitoring for timed properties.

Future work. Several avenues for future work are opened by this paper.

First, we believe it is important to study and delineate the set of enforceable timed properties. As shown informally by this paper, some timed properties should be characterized as non-enforceable. For this purpose, an enforceability condition should be defined and used to delineate enforceable properties. Such a criterion should ideally also be expressible on timed automata. We conjecture that several enforceability notions exist. Some notions depend on the underlying mechanism used to enforce properties. We believe that there is also one (formalism-independent) enforceability notion that stems only from the physical time constraints faced by enforcement mechanisms.

Note that even for properties which are non-enforceable, the enforcement monitors proposed in this paper can be built, which may not be able to correct some input sequences, but their outputs are always sound.

Properties are currently defined with timed automata. We consider synthesizing enforcement mechanisms from more expressive formalisms. For instance, we will consider formalisms such as context-free timed languages (which can be useful for recursive specifications) or introduce data into requirements (which can be useful in some application domains). Implementing efficient enforcement monitors is another important aspect and should be done w.r.t. a particular application domain.

We implemented the tool in Python with the objectives of i) making a quick prototype that shows feasibility of enforcement monitoring in a timed context, and ii) reusing some existing UPPAAL libraries. In the future, we will consider implementing our enforcement monitors in other languages such as C or Java, and we expect even better performance and a more stand-alone implementation.

Alternative enforcement primitives can be afforded to timed retardants, which could be of interest in some application domains. For instance, we could relax the constraint of only augmenting delays of events. For instance, time retardants that delay the total duration of the observation (while being allowed to shorten the delay of some events) have yet to be studied. Suppressing events also can be considered, by erasing some events which are stored in the memory. An event should be suppressed if it is not possible to satisfy the property in the future, whatever is the remainder of the input sequence (i.e. the TA has reached q nonaccepting state from which no accepting states can be reached). Formalizing suppression is however quite involved, requiring to redefine relations between input and output sequences which impacts on transparency.

Also related to expressiveness is the question of how the set of timed enforceable properties is impacted when the underlying memory is limited and/or the primitive operations endowed to the monitor are modified.

A Proofs

A.1 Proof of Proposition 3 -item 1 (physical constraints)

We shall prove that, given a property ϕ, the associated enforcement function Eϕ : (R ≥0 × Σ) * × R ≥0 → (R ≥0 × Σ) * defined as per Definition 8 satisfies the physical constraints (Phy1) and (Phy2). That is, we shall prove that:

∀σ ∈ (R ≥0 × Σ) * , ∀t, t ∈ R ≥0 : t ≤ t =⇒ Eϕ(σ, t) Eϕ(σ, t ), (Phy1) ∀σ ∈ (R ≥0 × Σ) * , ∀t ∈ (R ≥0 × Σ) * : time(Eϕ(σ, t)) ≤ t. (Phy2)
-Proof that the enforcement function satisfies (Phy1).

Let us consider σ ∈ (R ≥0 × Σ) * , t, t ∈ R ≥0 , such that t ≤ t . We will prove that there exists o ∈ (R ≥0 × Σ) * s.t Eϕ(σ, t ) = Eϕ(σ, t) • o. The fact that Eϕ satisfies (Phy1) is a direct consequence of the following observations:

-∀σ ∈ (R ≥0 × Σ) * , ∀t, t ∈ R ≥0 : t ≤ t =⇒ obs(σ, t) obs(σ, t ), i.e., obs is monotonic in its second argument; -∀w, w ∈ (R ≥0 × Σ) * : w w =⇒ store(w) store(w ), i.e., store is monotonic; -∀σ, σ ∈ (R ≥0 × Σ) * , ∀t ∈ R ≥0 : σ σ =⇒ obs(σ, t) obs(σ , t), i.e., obs is monotonic in its first argument. -Proof that the enforcement function satisfies (Phy2).

From Definition 8, since Eϕ(σ, t) = obs Π 1 store(obs(σ, t)) , t , from the definition of obs and the property of obs that ∀σ : time(obs(σ, t)) ≤ t, applied to Π 1 (store (obs (σ, t))), we can conclude that time(Eϕ(σ, t)) ≤ t. Thus, Eϕ satisfies (Phy2).

A.2 Proof of Proposition 3 -item 2 (soundness and transparency)

We shall prove that, given a property ϕ, the associated enforcement function Eϕ : (R ≥0 × Σ) * × R ≥0 → (R ≥0 ×Σ) * as per Definition 8 is sound and transparent as per Definitions 7, i.e., Eϕ satisfies the constraints (Snd) and (Tr).

Recall that Eϕ : (R ≥0 × Σ) * × R ≥0 → (R ≥0 × Σ) * is defined as:

Eϕ(σ, t) = obs Π 1 store(obs(σ, t)) , t .

where: From (Snd) and (Tr), we define the constraints that hold for a particular word σ and a particular time instant t (i.e., universal quantifications are removed). We denote these propositions by (Snd) σ,t and (Tr) σ,t respectively. Thus, we shall prove that Eϕ satisfies (Snd) σ,t and (Tr) σ,t for any σ ∈ (R ≥0 × Σ) * and t ∈ R ≥0 . For this purpose, we perform an induction on the length of σ.

-function obs : (R ≥0 × Σ) * × R ≥0 → (R ≥0 × Σ) * is the observation function defined in Sec. 2, -function store : (R ≥0 × Σ) * → (R ≥0 × Σ) * × (R ≥0 × Σ) * is
Induction Basis. Let us suppose that |σ| = 0, thus σ = in (R ≥0 × Σ) * . First, we have ∀t ∈ R ≥0 : obs(σ, t) = . Second, we have store( ) = ( , ). Consequently, we have ∀t ∈ R ≥0 : Eϕ(σ, t) = . We now prove that, at any time t ∈ R ≥0 , Eϕ satisfies (Snd) ,t and (Tr) ,t , successively.

-For σ = , we have ∀t ∈ R ≥0 : Eϕ(σ, t) = . Thus, Eϕ satisfies (Snd) ,t , for any time t ∈ R ≥0 .

-Since obs( , t) = and d , we have ∀t ∈ R ≥0 : Eϕ( , t) d . That is, Eϕ satisfies (Tr) ,t , for any time t ∈ R ≥0 .

Induction

Step. Let us consider n ∈ N and suppose that for any σ ∈ (R ≥0 × Σ) * with |σ| ≤ n, any t ∈ R ≥0 , Eϕ satisfies (Snd) σ,t and (Tr) σ,t .

Let us now prove that for any σ ∈ (R ≥0 × Σ) * with |σ | = n + 1, for any t ∈ R ≥0 , Eϕ satisfies (Snd) σ ,t and (Tr) σ ,t . For this purpose, let us consider some input timed word σ with |σ | = n + 1. Thus σ = σ • (δ, a) for some σ with |σ| = n, δ ∈ R ≥0 and a ∈ Σ. Let us consider some time instant t ∈ R ≥0 .

We distinguish two cases according to whether the sum of delays of the timed word σ • (δ, a) is greater than t or not, i.e., whether time(σ • (δ, a)) > t or not.

-Case time(σ • (δ, a)) > t. In this case, obs(σ • (δ, a), t) = obs(σ, t). Consequently, Eϕ(σ • (δ, a), t) = obs Π 1 store(obs(σ • (δ, a), t)) , t = Eϕ(σ, t). From the induction hypothesis, we directly deduce that Eϕ satisfies (Snd) σ ,t and (Tr) σ ,t .

-Case time(σ • (δ, a)) ≤ t. In this case obs(σ • (δ, a), t) = σ • (δ, a).

We distinguish two cases, based on whether K = ∅, or not.

- From the definition of store, we have store(σ

A.3 Proof of Proposition 4

We shall prove that, given a property ϕ, the associated enforcement function Eϕ : (R ≥0 × Σ) * × R ≥0 → (R ≥0 × Σ) * as per Definition 8 satisfies the optimality constraint (Op) (from Definition 4).

∀σ ∈ (R ≥0 × Σ) * , ∀t ∈ R ≥0 : Eϕ(σ, t) = ∧ Eϕ(σ, t) |= ϕ =⇒ ∃wmx, w ∈ (R ≥0 × Σ) * : wmx = max ϕ ≺, (Eϕ(σ, t)) ∧Eϕ(σ, t) = wmx • w ∧ time(w) = min{time(w ) | delay(w (1)) ≥ time(σ [1•••|Eϕ(σ,t)|] ) -time(wmx) ∧wmx • w |= ϕ ∧ Π Σ (w ) = Π Σ (w)}.
where the function Eϕ is defined in Sec. 3.2.1 and recalled in the previous proof.

From (Op), we define the constraint dedicated to a particular word σ and a particular time instant t (i.e., universal quantifications are removed). We denote this proposition by (Op) σ,t . Thus, we shall prove that Eϕ satisfies (Op) σ,t for any σ ∈ (R ≥0 × Σ) * and t ∈ R ≥0 . For this purpose, we perform an induction on the length of σ.

Induction Basis. Let us suppose that |σ| = 0, thus σ = in (R ≥0 × Σ) * . First, we have ∀t ∈ R ≥0 : obs(σ, t) = . Second, we have store( ) = ( , ). Consequently, we have ∀t ∈ R ≥0 : Eϕ(σ, t) = . For σ = , we have ∀t ∈ R ≥0 : Eϕ(σ, t) = . Thus, Eϕ vacuously satisfies (Op) ,t , for any t ∈ R ≥0 .

Induction

Step. Let us consider n ∈ N and suppose that for any σ ∈ (R ≥0 × Σ) * with |σ| ≤ n, any t ∈ R ≥0 , Eϕ satisfies (Op) σ,t .

Let us now prove that, for any σ ∈ (R ≥0 × Σ) * with |σ | = n + 1, for any t ∈ R ≥0 , Eϕ satisfies (Op) σ ,t . For this purpose, let us consider some input timed word σ with |σ | = n+1. Thus σ = σ •(δ, a) for some σ with |σ| = n, δ ∈ R ≥0 and a ∈ Σ. Let us consider some time instant t ∈ R ≥0 .

We distinguish two cases according to whether the sum of delays of the timed word σ • (δ, a) is greater than t or not, i.e., whether time(σ • (δ, a)) > t or not.

-Case time(σ • (δ, a)) > t. In this case, obs(σ (δ, a), t) = obs(σ, t). Consequently, Eϕ(σ • (δ, a), t) = obs Π 1 store(obs(σ • (δ, a), t)) , t = Eϕ(σ, t). From the induction hypothesis, we directly deduce that Eϕ satisfies (Op) σ ,t .

-Case time(σ • (δ, a)) ≤ t. We have obs(σ • (δ, a), t) = σ • (δ, a).

We distinguish two cases, based on whether K = ∅, or not, where K = κϕ(time(σ) + δ, σs, σc • (δ, a)).

-Case K = ∅. From the definition of store, we have store(σ • (δ, a)) = (σs, σc • (δ, a)), and Π 1 store(σ • (δ, a)) = σs. We also have Π

A.4.1 Some Remarks

Remark 12 In the following proofs, without loss of generality, we assume that at any time only one of the rules of the enforcement monitor applies. This simplification does not come at the price of reducing the generality nor the validity of the proofs because i) the store and dump rules of the enforcement monitor assign different variables and do not rely on the same conditions, and ii) the operations of enforcement monitors are assumed to be executed in zero time. The considered simplification however reduces the number of (equivalent cases) in the following proofs.

Remark 13 Between the occurrence of two (input or output) events the configuration of the enforcement monitor evolves according to the idle rule (since it is the rule with lowest priority). To simplify notations we will use a rule to simplify the representation of

E ioo ∈ (R ≥0 × Σ) ∪ { } × Op × (R ≥0 × Σ) ∪ { } stating that σ • ( , idle(δ 1 ), ) • ( , idle(δ 2 ), ) • σ is equivalent to σ • ( , idle(δ 1 + δ 2 ), ) • σ for any σ, σ ∈ (R ≥0 × Σ) ∪ { } × Op × (R ≥0 × Σ) ∪ { } and δ 1 , δ 2 ∈ R ≥0 .
Thus for E ioo we will only consider sequences of (R ≥0 × Σ) ∪ { } × Op × (R ≥0 × Σ) ∪ { } where delays appearing in the idle operation are maximal (i.e., there is no sequence of two consecutive events with an idle operation).

A.4.2 Some notations

Since it is assumed that at most one rule of the enforcement monitor applies at any time, let us define the functions config in , configout : (R ≥0 × Σ) * × R ≥0 → C E that give respectively the input and output configurations of an enforcement monitor reading an input sequence at some time instant. More formally, given some σ

∈ (R ≥0 × Σ) * , t ∈ R ≥0 : -config in (σ, t) = c t σ such that c E 0 w(σ,t) → * c t σ where w(σ, t) def = min {ioo E ioo (σ, t) | timeop(ioo) = t}; -configout(σ, t) = c t σ such that c E 0 E ioo (σ,t)
→ * c t σ . Observe that, when at some time instant, only the idle rule applies, config in (σ, t) = configout(σ, t) holds.

Moreover, for any two t, t ∈ R ≥0 such that t ≥ t, we note E(σ, t, t ) for E(σ, t ) \ E(σ, t), i.e., the output sequence of an enforcement monitor between t and t .

A.4.3 Some Intermediate Lemmas

Before tackling the proof of Proposition 5, we give a list of lemmas that describes the behavior of an enforcement monitor, describing the configurations or the output at some particular time instant for some input and memory content.

Similarly to the first physical constraint, the following lemma states that the enforcement monitor cannot change what it has output. More precisely, when the enforcement monitor is seen as function E, the output is monotonic w.r.t. .

Lemma 1 (Monotonicity of the outputs of enforcement monitors) Function

E : (R ≥0 × Σ) * × R ≥0 → (R ≥0 × Σ) * is monotonic in its second parameter: ∀σ ∈ (Σ × R ≥0 ) * , ∀t, t ∈ R ≥0 : t ≤ t =⇒ E(σ, t) E(σ, t ).
The lemma states that for any input sequence σ, if we consider two time instants t, t such that t ≤ t , then the output of the enforcement monitor at time t is a prefix of the output at time t .

Proof (of Lemma 1)

The proof directly follows from the definitions of the function E associated to an enforcement monitor (see Sec. 3.4, p. 19) which directly depends on E ioo , which is itself monotonic over time (because of the definition of enforcement monitors).

As a consequence, one can naturally split the output of the enforcement monitor over time, as it is stated by the following corollary.

Corollary 1 (Separation of the output of the enforcement monitor over time)

∀σ ∈ (R ≥0 × Σ) * , ∀t 1 , t 2 , t 3 ∈ R ≥0 : t 1 ≤ t 2 ≤ t 3 =⇒ E(σ, t 1 , t 3 ) = E(σ, t 1 , t 2 ) • E(σ, t 2 , t 3 ).
The corollary states that for any sequence σ input to E, if we consider three time instants t 1 , t 2 , t 3 ∈ R ≥0 such that t 1 ≤ t 2 ≤ t 3 , the output of E between t 1 and t 3 is the concatenation of the output between t 1 and t 2 and the output between t 2 and t 3 .

Proof (of Corollary 1)

The corollary directly follows from Lemma 1.

The following lemma states that, at some time instant t, the output of the enforcement monitor only depends on what has been observed until time t. In other words, the enforcement monitor can work in an online fashion.

Lemma 2 (Dependency of the output on the observation only)

∀σ ∈ (R ≥0 × Σ) * , ∀t ∈ R ≥0 : E(σ, t) = E(obs(σ, t), t).
Proof (of Lemma 2) The proof of the lemma directly follows from the definitions of E ioo (Definition 10, p. 20) and obs (in Sec. 2). Indeed, using obs(σ, t) = obs(obs(σ, t), t), we deduce that E ioo (σ, t) = E ioo (obs(σ, t), t), for any σ ∈ (R ≥0 × Σ) * and t ∈ R ≥0 . Using E(σ, t) = Π 3 (E ioo (σ, t)), we can deduce the expected result.

The following lemma indicates the value of the store variable inside the configurations at some special time instants (corresponding to the time necessary to read prefixes of the input sequence).

Lemma 3 (Values of config in when reading events)

∀σ, σ ∈ (R ≥0 × Σ) * , ∀t ∈ R ≥0 : σ σ ∧ t = time(σ ) =⇒ config in (σ, t) = ( , , time(last(σ )), , , ).
Proof (of Lemma 3) The proof can be done using a straightforward induction on the length of the maximal considered prefix σ of σ. Moreover, the proof uses the facts that between two prefixes of the input sequence, i) no modification is brought to the store variable, and ii) the store variable is reset upon the store of each event.

The following lemma states that only the memory content σs and the value of the dump variable influence the output of the enforcement monitor. More specifically, if, after reading some sequence, an enforcement monitor reaches some configuration, its future output is fully determined by the memory content σs(containing the corrected sequence) and the value of the dump variable (d), during the total time needed to output it.

Lemma 4 (Values of configout when releasing events)

∀σ, σs, σc ∈ (R ≥0 × Σ) * , ∀t ∈ R ≥0 , ∀s, d, mt ∈ R ≥0 , ∀q ∈ Q : t ≥ time(σ) ∧ configout(σ, t) = (σs, σc, s, d, mt, q) =⇒ ∀σ s σs, ∃σ c ∈ (R ≥0 × Σ) * , ∃s ∈ R ≥0 , ∃m t ∈ R ≥0 , ∃q ∈ Q : configout(σ, t + time(σ s ) -d) = (σs \ σ s , σ c , s , 0, m t , q ).
The lemma states that whatever is the output configuration (σs, σc, s, d, mt, q) reached by reading some input sequence σ at some time instant t ≥ time(σ), then for any prefix σ s of σs the output configuration reached at time t + time(σ s ) -d (we add the time needed to read σ s minus the value of the dump clock) is such that σ s has been released from the memory (the memory is σs \ σ s ) and the value of the dump variable has just been reset to 0.

Proof (of Lemma 4)

The proof is a straightforward induction on the length of σ s . It uses the fact that the considered configurations occur at time instants greater than time(σ), hence implying that no input event can be read any more. Consequently, following the definition of the enforcement monitor (Definition 9, p. 18), on the configurations of the enforcement monitor, only the idle and dump rules apply. Between time(σ s ) and time(σ s • (δ, a)) where σ s σ s • (δ, a) σs, the configuration of the enforcement monitor evolves only using the idle rule (no other rule applies) until config in (σ, t + time(σ s )) = (σs \ σ s , σc, s + δ, δ, mt, q) with σs \ σ s . The dump rule is then applied to get the following derivation (σs \ σ s , σc, s + δ, δ, mt, q) /dump(δ,a)/

→

(σs \ (σ s • (δ, a)), σc, s + δ, 0, mt, q).

The following lemma states that when an enforcement monitor has nothing to read in input anymore, what is output is the observation of its memory content over time. The lemma states that, if after some time t, after reading an input sequence σ, the enforcement monitor is in an output configuration that contains σs as a memory content, then whatever is the prefix σ s of σs we consider, the output of the enforcement monitor between t and t + time(σ s ) is the observation of σ s .

Proof (of Lemma 5)

The proof is performed by induction on the length of σ s and uses Lemma 4.

-Case |σ s | = 0. In this case, σ s = and since time( ) = 0 and E(σ, t, t -d) is not defined, the lemma vacuously holds. -Induction case. Let us suppose that the lemma holds for all prefixes σ s of some maximum length n ∈ [0, |σs|-1]. Let us consider σ the prefix of σs of length n+1. On the one hand, at time t+time(σ )-d, i.e., when t = time(σ ) -d, according to Lemma 4, we have configout(σ, t + time(σ ) -d) = ((δ, a), σc, s, 0, mt, q) for some s, mt ∈ R ≥0 and σc ∈ (R ≥0 × Σ) * . On the other hand, let us consider some t ∈ [0, δ], we have: A.5 Proof of Proposition 5: Relation between Enforcement Function and Enforcement Monitor

E(σ,
Proof. We shall prove that, given a property ϕ, the associated enforcement monitor as per Definition 9

(p. 18) implements the associated enforcement function Eϕ : (R ≥0 × Σ) * × R ≥0 → (R ≥0 × Σ) * as per Definition 8 (p. 12). That is:

∀σ ∈ (R ≥0 × Σ) * , ∀t ∈ R ≥0 : Eϕ(σ, t) = E(σ, t).
The proof is done by induction on the length of the input timed word σ.

Induction Basis. Let us suppose that |σ| = 0, thus σ = in (R ≥0 × Σ) * . On the one hand, we have ∀t ∈ R ≥0 : Eϕ(σ, t) = . On the other hand, the word E ioo ( , t) over the input-operation-output alphabet is such that ∀t ∈ R ≥0 : E ioo ( , t) = . Thus, according to the definition of the enforcement monitor, store-ϕ and store-ϕ rules cannot be applied. Consequently, the memory of the enforcement monitor remains empty as in the initial configuration. It follows that the dump rule cannot be applied. We have then

C E 0 / idle(t)/
→ ( , , t, t, 0, q), and thus E( , t) = .

Induction

Step. Let us suppose that Eϕ(σ, t) = E(σ, t) for any timed word σ ∈ (R ≥0 × Σ) * of some length n ∈ N, at any time t ∈ R ≥0 . Let us now consider some input timed word σ • (δ, a) for some σ ∈ (R ≥0 × Σ) * with |σ| = n, δ ∈ R ≥0 , and a ∈ Σ. We want to prove that Eϕ(σ • (δ, a), t) = E(σ • (δ, a), t), at any t ∈ R ≥0 . Let us consider some time instant t ∈ R ≥0 . We distinguish two cases according to whether time(σ • (δ, a)) > t or not, that is whether σ • (δ, a) is completely observed or not at time t.

-Case time(σ • (δ, a)) > t. In this case, obs (σ • (δ, a), t) = obs(σ, t), i.e., at time t, the observations of σ and σ • (δ, a) are identical. On the one hand, we have: Eϕ (σ • (δ, a), t) = obs Π 1 store(obs(σ • (δ, a), t)) , t = obs Π 1 store(obs(σ, t)) , t = Eϕ(σ, t). On the other hand, regarding the enforcement monitor, since obs σ • (δ, a), t = obs(σ, t), using Lemma 2 (p. 36), we obtain E(σ • (δ, a), t) = E(σ, t). Using the induction hypothesis, we can conclude that Eϕ(σ • (δ, a), t) = E(σ • (δ, a), t).

Let us examine E(σ • (δ, a), t). We have:

B Implementation of Store Processes

We provide a brief description related to how the store process, which processes the input events (checking for the satisfaction of the property and computing delays) is implemented.

B.1 Implementation of StoreProcess safety

We now describe the implementation of StoreProcess safety used by an enforcement monitor for safety properties. The StoreProcess safety first parses the input model, and performs the necessary initialization. For each event of the trace in order, first the automaton representing the input trace is updated with the new event.

Then the updates function is invoked, with the current state information and the event. The updates function returns ff if an accepting state is not reachable upon the event (δ, a) from the current state. In case if an accepting state is reachable, then the updates function returns the optimal delay with information about the state that is reachable. Before continuing with the next event, the StoreProcess updates the current state information. In the StoreProcess safety , the execution time of updates is measured. The StoreProcess safety keeps track of the total time of updates, by adding the updates time measured after each event to the total time, which is returned as a result of invoking the StoreProcess safety .

B.2 Implementation of StoreProcess co-safety

The StoreProcess co-safety is implemented following the algorithm and steps described in [START_REF] Pinisetty | Runtime enforcement of timed properties[END_REF]. Below we provide an abstract description of the code implementing the updatecs function. The updatecs function takes a timed word (the events read by the enforcement monitor), and returns a new delay for each input event, if an accepting state is reachable for the given input timed word. First, all paths starting from the initial state for the given input sequence are computed. Then the set of all accepting paths is computed. In each path, if the location in the last state is accepting, then the path is accepting, and is a non-accepting path otherwise.

If the set of accepting paths is empty, then updatecs returns ff. If there are accepting paths, for each state in the path, a corresponding delay is computed, and the paths whose sums of delays are minimal are filtered. Among these paths, one path is chosen according to the lexical order, and the delays corresponding to this path are returned as the result.

Fig. 1

 1 Fig. 1 Enforcement mechanism.

  A safety TA for ϕ 1 .

  A co-safety TA for ϕ 2 .

  A TA for ϕ 4 .

Fig. 2

 2 Fig. 2 Examples of TA modeling timed properties.

Fig. 3

 3 Fig. 3 Enforcement function Eϕ

Fig. 4

 4 Fig. 4 Evolution of the enforcement function for ϕ 3 .

Fig. 5

 5 Fig. 5 Evolution of the enforcement function for ϕ 4 .

Fig. 6

 6 Fig. 6 Execution of an enforcement monitor

Fig. 8

 8 Fig. 8 Experimental framework

Fig. 9

 9 Fig.9Length of the input (Vs) total execution time of update.

Fig. 10

 10 Fig. 10 For ϕ 1 cs : Length of the input trace (Vs) total execution time of update.

  defined as follows in Sec. 3.2.1: store( ) = ( , ) store(σ • (δ, a)) =    (σs • min lex,time K, ) if K = ∅ (σs, σc • (δ, a)) otherwise with (σs, σc) = store(σ) K = κϕ(time(σ) + δ, σs, σc • (δ, a)) with κϕ(T, σs, σc) def = {w ∈ (R ≥0 × Σ) * | w d σc ∧ |w| = |σc| ∧ σs • w |= ϕ ∧ delay(w(1)) ≥ T -time(σs))}.

  Case K = κϕ(time(σ) + δ, σs, σc • (δ, a)) = ∅. From the definition of store, we have store(σ • (δ, a)) = (σs, σc • (δ, a)), and Π 1 store(σ • (δ, a)) = σs. We also have Π 1 store(σ) = σs. From the definition of Eϕ, we have Eϕ(σ • (δ, a), t) = Eϕ(σ, t). From the induction hypothesis, we deduce that Eϕ satisfies (Snd) σ ,t and (Tr) σ ,t . -Case K = κϕ(time(σ) + δ, σs, σc • (δ, a)) = ∅.

Lemma 5 ∀σ

 5 , σs, σc ∈ (R ≥0 × Σ) * , ∀t ∈ R ≥0 , ∀s, d, mt ∈ R ≥0 , ∀q ∈ Q : t ≥ time(σ) ∧ configout(σ, t) = (σs, σc, s, d, mt, q) =⇒ ∀σ s ∈ (R ≥0 × Σ) * , ∀t ∈ R ≥0 : σ s σs ∧ d ≤ t ≤ time(σ s ) =⇒ E(σ, t, t + t -d) = obs(σ s , t ).

  t, t+time(σ )+t -d) = E(σ, t, t+time(σ )-d)•E(σ, t+time(σ )-d, t+time(σ )+t -d).Using the induction hypothesis, we find E(σ, t, t + time(σ ) -d) = obs(σ , time(σ )) = σ . Using the semantics of the enforcement monitor (dump and idle rules), we obtain E(σ, t+time(σ )+t -d) = obs((δ, a), t +d). Thus, E(σ, t, t+time(σ )+t -d) = σ •obs((δ, a), t +d) = obs(σ •(δ, a), t + d).

E

  (σ • (δ, a), t) = E(σ • (δ, a), time(σ • (δ, a)) -t ) •E(σ • (δ, a), time(σ • (δ, a)) -t , time(σ • (δ, a))) •E(σ • (δ, a), time(σ • (δ, a)), t).Let us examine E(σ, t). We have:E(σ, t) = E(σ, time(σ • (δ, a)) -t ) •E(σ, time(σ • (δ, a)) -t , time(σ • (δ, a))) •E(σ, time(σ • (δ, a)), t).Observe thatE(σ • (δ, a), time(σ • (δ, a)) -t ) = E(σ, time(σ • (δ, a)) -t ) because obs(σ • (δ, a), time(σ • (δ, a)) -t ) = σaccording to the definition of obs. Moreover, E(σ • (δ, a), time(σ • (δ, a)) -t , time(σ • (δ, a))) = since only the idle rule applies during the considered time interval. Furthermore, according to Lemma 5, since configout(σ•(δ, a), time(σ•(δ, a))) = (σs•σ c , , 0, d, m t , q ), we get E(σ • (δ, a), time(σ • (δ, a)), t) = obs(σs • σ c , t -time(σ • (δ, a)) + d).Now we further distinguish two more sub-cases, based on whether time(σs• σ c ) > t -time(σ • (δ, a)) + dor not (whether all the elements in the memory can be released as output by time t or not).• Case time(σs• σ c ) > t -time(σ • (δ, a)) + d.We further distinguish two more sub-cases based on whether time(σs) > t -time(σ • (δ, a)) + d, or not. • Case time(σs) > t -time(σ • (δ, a)) + d.In this case, we know that obs(σs• σ c , ttime(σ • (δ, a)) + d) = obs(σs, t -time(σ • (δ, a)) + d).Hence, we can derive that E(σ • (δ, a), t) = E(σ, t). Also, from the induction hypothesis, we know that E(σ, t) = Eϕ(σ, t).Regarding Eϕ, we have store(σ•(δ, a)) = Π 1 store(σ) •min lex,time K. Moreover Eϕ(σ • (δ, a), t) = obs Π 1 store(obs(σ, t)) , t = obs(Π 1 store(σ) • min lex,time K, t).We can have Eϕ(σ • (δ, a), t) = Π 1 store(σ) • O where O min lex,time K which is equal to Eϕ(σ, t)•O, only if the delays computed by the update function are different from the delays computed by Eϕ. This would violate the induction hypothesis stating that E(σ, t) = Eϕ(σ, t). Hence, we have Eϕ(σ • (δ, a), t) = obs( Π 1 store(σ) , t) = Eϕ(σ, t). Thus, Eϕ(σ • (δ, a), t) = E(σ • (δ, a), t). • Case time(σs) ≤ t-time(σ•(δ, a))+d. In this case, we can follow the same reasoning as in the previous case to obtain the expected result. • Case time(σs • σ c ) ≤ t -time(σ • (δ, a)) + d. In this case, similarly following Lemma 5 (p. 36), we have E(σ • (δ, a), time(σ • (δ, a)), t) = obs(σs • σ c , t -time(σ • (δ, a) + d) = σs • σ c . We can also derive that E(σ, time(σ • (δ, a)), t) = σs. Consequently, we have E(σ • (δ, a), t) = E(σ, t) • σ c . From the induction hypothesis, we know that Eϕ(σ, t) = E(σ, t), and we have E(σ • (δ, a), t) = Eϕ(σ, t) • σ c . We have store(σ • (δ, a)) = Π 1 store(σ) • min lex,time K, and thus Eϕ(σ • (δ, a), t) = obs Π 1 (store (σ)) • min lex,time K, t . Hence, in this case, we have Eϕ(σ • (δ, a), t) = store(σ) • min lex,time K = Eϕ(σ, t) • min lex,time K, since the delays computed for the subsequence σc • (δ, a) by Eϕ and E are equal. Finally, we have Eϕ(σ • (δ, a), t) = E(σ • (δ, a), t).

  = 10 for ϕ 1.2 s , n = 20 for ϕ1.3 s . Property ϕ 2 s belongs to the precedence pattern. It expresses that "A sequence of n a-actions enables action b after a delay of k time units".Results and analysis. Results of the performance analysis of our running example properties are reported in Table1. The entry t update indicates the total execution time of the update function, and the entry t avg is the average time per call. From the results presented in Table

	1.1 s , ϕ 1.2 s	and ϕ 1.3 s , each varying in the value of n: n = 2 for
	ϕ 1.1
	Following this pattern, the considered properties are ϕ 2.1 s , ϕ 2.2 s	and ϕ 2.3 s , each varying in
	the value of n: n = 1 for ϕ 2.1 s , n = 5 for ϕ 2.2 s , and n = 10 for ϕ 2.3 s .

s , n

Table 1

 1 Performance analysis of enforcement monitors for safety properties

			ϕ 1.1 s		ϕ 1.2 s	ϕ 1.3 s
	|tr|	t update	t avg		t update	t avg	t update	t avg
	10, 000		8.6306	0.000863		8.008	0.00080	8.106	0.000810
	20, 000		16.157	0.000807		16.538	0.000828	16.887	0.000844
	30, 000		25.251	0.000841		24.855	0.000828	24.3794	0.00812
	40, 000		32.199	0.000804		33.947	0.000848	33.619	0.000840
	50, 000		39.982	0.000799		44.704	0.000854	43.314	0.000866
	60, 000		50.785	0.000846		49.616	0.000826	53.521	0.000892
	70, 000		55.821	0.000797		58.317	0.000833	60.928	0.000870
	80, 000		66.080	0.000826		66.876	0.000835	66.461	0.000830
	90, 000		74.082	0.000823		76.327	0.000848	76.807	0.000853
			ϕ 2.1 s		ϕ 2.2 s	ϕ 2.3 s
	|tr|	t update	t avg		t update	t avg	t update	t avg
	10, 000		8.589	0.000858		8.019	0.000801	8.050	0.000805
	20, 000		17.435	0.000871		16.603	0.000830	17.472	0.000873
	30, 000		26.760	0.000892		25.507	0.000850	24.353	0.000811
	40, 000		36.956	0.000923		33.576	0.000839	32.811	0.000820
	50, 000		43.806	0.000876		42.955	0.000859	41.141	0.000822
	60, 000		55.410	0.000923		51.417	0.000856	51.550	0.000859
	70, 000		62.816	0.000897		59.677	0.000852	59.572	0.000851
	80, 000		70.282	0.000878		66.800	0.000835	67.450	0.000843
	90, 000		80.659	0.000896		73.423	0.000815	76.137	0.000845
		0.2	0.4	0.6	0.8	1
						•10 5

Table 2

 2 Performance analysis of enforcement monitors for co-safety properties

			ϕ 1.1 cs			ϕ 1.2 cs
	|tr|	t update	t avg	t last	t update	t avg	t last
	100	3.332	0.0333	0.0776	3.4099	0.034	0.080
	200	12.838	0.0641	0.148	13.27	0.0663	0.155
	300	29.926	0.0997	0.231	30.687	0.102	0.229
	400	51.925	0.129	0.303	53.280	0.133	0.310
	500	79.66	0.159	0.372	81.91	0.163	0.382
	600	115.05	0.191	0.448	117.24	0.19	0.45
	700	159.64	0.228	0.530	161.97	0.231	0.53
	800	206.95	0.258	0.608	212.64	0.265	0.62
	900	262.2	0.291	0.683	267.61	0.297	0.695
	4.2 Performance evaluation of the update function for co-safety properties

  • (δ, a)) = ((σs • min lex,time K, ), and Π 1 store(σ • (δ, a)) = (σs•min lex,time K). We distinguish two cases based on whether time(σs•min lex,time K) > t or not.-Case time(σs • min lex,time K) > t. We further distinguish two more cases based on whether time(σs) > t or not. -Case time(σs) > t. In this case, we have obs(σs • min lex,time K, t) = obs(σs, t). Thus we have Eϕ(σ • (δ, a), t) = Eϕ(σ, t). So, from the induction hypothesis, we deduce that Eϕ satisfies (Snd) σ ,t and (Tr) σ ,t . -Case time(σs) ≤ t. In this case we have Eϕ(σ•(δ, a), t) = σs•O, where O ≺ min lex,time K. From the definition of K and κϕ we know that σs • min lex,time K ∈ ϕ. Since ∀t ≥ time(σs•min lex,time K) and Eϕ(σ•(δ, a)) = σs•min lex,time K, Eϕ satisfies (Snd) σ ,t , for any t ∈ R ≥0 . From the induction hypothesis, we know that σs d σ. From the definition of K and κϕ, and using the induction hypothesis, we can conclude that σs•min lex,time K d σ • (δ, a), and thus we also have σs • O d σ • (δ, a). Thus Eϕ satisfies (Tr) σ ,t . -Case time(σs•min lex,time K) ≤ t. In this case, we have Eϕ(σ•(δ, a), t) = σs•min lex,time K. From the definition of K and κϕ we know that σs • min lex,time K ∈ ϕ. Thus Eϕ satisfies (Snd) σ ,t . From the induction hypothesis, we know that σs d σ. From the definition of K and κϕ, and using the induction hypothesis, we can conclude that σs • min lex,time K d σ • (δ, a). Thus Eϕ satisfies (Tr) σ ,t .

  From the induction hypothesis, we deduce that Eϕ satisfies (Op) σ ,t .-Case K = ∅. From the definition of store, we have store(σ • (δ, a)) = ((σs • min lex,time K, ), Preliminaries to the Proof of Proposition 5: Characterizing the Configurations of Enforcement MonitorsWe first convey some remarks (Sec. A.4.1), define some notions (Sec. A.4.2) and lemmas (Sec. A.4.3) related to the configurations of enforcement monitors.

1 store(σ) = σs. From the definition of Eϕ, we have Eϕ(σ • (δ, a), t) = Eϕ(σ, t). and Π 1 store(σ • (δ, a)) = (σs • min lex,time K). We distinguish two cases based on whether time(σs • min lex,time K) > t or not.

-Case time(σs • min lex,time K) > t. We further distinguish two more cases based on whether time(σs) > t or not.

-Case time(σs) > t. We have obs(σs • min lex,time K, t) = obs(σs, t). Thus, we have Eϕ(σ • (δ, a), t) = Eϕ(σ, t). Hence, from the induction hypothesis, we deduce that Eϕ satisfies (Op) σ ,t . -Case time(σs) ≤ t. We have Eϕ(σ

• (δ, a), t) = σs • O, where O ≺ min lex,time K.

According to the definition of store, σs • O |= ϕ. Thus, Eϕ vacuously satisfies (Op) σ ,t . -Case time(σs • min lex,time K) ≤ t. We have Eϕ(σ • (δ, a), t) = σs • min lex,time K. From the definition of K and κϕ, we know that σs • min lex,time K |= ϕ. From the definition of store, we know that σs is the maximal strict prefix of σs • min lex,time K, which satisfies ϕ. The last subsequence which again makes the output satisfy the property is min lex,time K. From the definition of K and κϕ, we also know that the delay(min lex,time K(1)) ≥ time(σ) + δtime(σs). Thus, we can conclude that Eϕ satisfies (Op) σ ,t .

A.4

As our experiments in Sec. 4 show, the computation time of the monitor upon the reception of an event is relatively low. Moreover, given some average computation time per event and a property, one can determine easily whether the computation time is negligible or not.

Observe that the notions of transparency and optimality in a timed context are interpretations of the historical notion of transparency when dealing with enforcement mechanisms as time retardants: the output sequence is a minimally-delayed prefix of the input sequence.

As one can observe, these definitions of safety and co-safety TAs slightly differ from the usual ones by expressing constraints on the initial state. As a consequence of these constraints, consistently with Definition 2, the empty and universal properties are ruled out from the set of safety and co-safety properties, respectively.

The pyuppaal and DBM libraries are provided by Aalborg University. They can be downloaded at http: //people.cs.aau.dk/ ˜adavid/python/.

-Case time(σ • (δ, a)) ≤ t. In this case, we have obs(σ • (δ, a), t) = σ • (δ, a) (i.e., σ • (δ, a) has been observed entirely). Using Lemma 3 (p. 36), we know that the configuration of the enforcement monitor at time time(σ • (δ, a)) is config in σ • (δ, a), time(σ • (δ, a)) = (σs, σc, δ, d, mt, qσ) for some σs, σc

) because of i) the definition of config in using the definition of E ioo and ii) the event (δ, a) has not been yet consumed through none of the store rules by the enforcement monitor at time time(σ • (δ, a)).

We distinguish two cases according to whether σc • (δ, a) can be delayed into a word satisfying ϕ or not, i.e., whether K = κϕ(time(σ) + δ, σs, σc • (δ, a)) = ∅, or not.

- Let us examine E(σ • (δ, a), t). We have:

Let us examine E(σ, t). We have:

Observe where:

-

→ q Thus configout(σ • (δ, a), time(σ • (δ, a)) = (σs • σ c , , 0, d, m t , q ). Let us consider t such that during time(σ • (δ, a)) -t and time(σ • (δ, a)), the enforcement monitor does not read any input nor produce any output, i.e., for all t ∈ [time(σ • (δ, a))t , time(σ • (δ, a))], config(t) is such that only the idle rule applies.