Runtime Verification of Contracts with Themulus

Abstract

Contracts regulating the behaviour of multiple interacting parties go beyond the notion of pure properties, but allow one to document and analyse the ideal behaviour. In this paper we build upon a real-time deontic logic allowing the description of such contracts and present a runtime verification tool for monitoring of such contracts. We present a verification algorithm used to monitor contracts written in this logic and an airport agreement is used as a case study to illustrate how such agreements and contracts can be monitored using our tool with reasonable processing costs.

Research partially supported by the Spanish MINECO/FEDER projects DArDOS (TIN2015-65845-C3-1-R) and FAME (RTI2018-093608-B-C31) and the Comunidad de Madrid project FORTE-CM (S2018/TCS-4314) co-funded by EIE Funds of the European Union.

1 Introduction

With the rise of multi-party systems and services, the formal notion of contracts or regulated interaction between participating parties has increased in importance. For many such situations, viewing a contract as a logical property which is not to be violated is sufficient—whether it is for the verification, monitoring or enforcement of the communication between parties. However, another view is that the notion of contracts should be first-class objects which speak about ideal behaviour but also cover the possibility that the actual behaviour does not match the ideal one and its consequences. Deontic logics [10] address precisely this aspect, typically using ideal-behaviour modalities such as obligations, permissions and prohibitions. Consider a multi-party system in which, whenever a file is downloaded, then the user should pay. From a deontic perspective, we would see an obligation to perform a pay action whenever we see a download action. Within the deontic logic, one can also express reparation clauses e.g. an obligation to pay a fine is added if the obligation to pay is not satisfied. Various approaches have been proposed in the literature for the formal reasoning about such deontic concepts e.g. defeasible logic in [11], event calculus-based in [12], dynamic logic style in $\mathcal {CL}$   [15] and automata-based in [13]. The common theme across these and other related approaches is looking at contracts as first-class entities which can be analysed and transformed independently of the systems they regulate enabling analysis such as conflict analysis or contract bias evaluation.

One recurring challenge across these approaches, beyond the deontic one, is that of addressing temporal issues [14], however, there has been limited work on deontic logic allowing reasoning about continuous time contracts, and no tools we are aware of. Recently, we have proposed Themulus   [2], a real-time deontic calculus to reason about contracts over continuous time. From a practical perspective, the use of the calculus for actual verification of system behaviour with respect to a contract raises challenges, particularly due to the real-time nature of the calculus. In this paper, we present some results proving the soundness of a runtime verification algorithm of contracts written in Themulus. We have implemented this algorithm on top of the runtime verification tool Larva [6] in order to enable real-world agreements to be monitored.

Fig. 1.

Operational Semantics transition rules 1/2

Fig. 2.

Operational Semantics transition rules 2/2

2 Contracts and Agents

In this section, we present some previous definitions published in [2]. We include them here to make the paper self-contained. We will assume a time domain $\mathbb {T}$ ranging over the non-negative reals¹. In order to deal with the recursion operator, we assume a set of variables $\mathsf {fvars}$ over which recursion will be defined.

Contracts regulate the behaviour of a number of agents, or parties running in parallel. In this section we present the notation we will use to describe these agents and their behaviour in order to be able to formalize contracts in the following sections.

Structurally, the underlying system consists of a number of indexed agents running in parallel, using variables A, $A'$ to represent the individual agents. The system as a whole will consist of the parallel composition of all agents indexed by a finite set $\mathcal I$ i.e. the system will be of the form $||_{i\in \mathcal{I}}A_{i}$. We will use variables $\mathcal{A}$, $\mathcal{A}'$ to denote the state of the system as a whole. Agents semantics are thus assumed to be represented as timed labelled transition systems:

• , for $a\in \mathsf {Act}$, indicates that agent A changes to $A'$ upon performing action a. As it is usual in process algebrae  [17], the execution of actions do not consume time. The transition indicates that agent A cannot perform action .

• , for $d>0\in \mathbb {T}$, indicates that agent A evolves to $A'$ after d time units pass.

2.1 Contract Syntax

Definition 1

The set of contract formulae denoted by (with variable to range over the contracts) is syntactically defined as follows:

$$\begin{array}{lrl} \varphi &{}\,::=\,&{} \top \mid \bot \mid {\mathcal {P}_{k}(a)[d]} \mid {\mathcal {O}_{k}(a)[d]} \mid {\mathcal {F}_{k}(a)[d]} \mid \mathsf {wait}(d) \mid \text {cond}_{k}(a)[d](\varphi _1,\varphi _2) \\ &{} \mid &{} \varphi _1; \varphi _2 \mid \varphi _1\wedge \varphi _2 \mid \varphi _1\vee \varphi _2 \mid \varphi _1\blacktriangleright \varphi _2 \mid \mathsf {rec\;}x.\varphi \mid x \end{array}$$

where $a\in \mathsf {Act}$, $x\in \mathsf {fvars}$, $k\in \mathcal{I}$ and $d\in \mathbb {T}\cup \{\infty \}$.

The basic formulae $\top$ and $\bot$ indicate, respectively, the contracts that are trivially satisfied and violated. Then we have the operators that represent the modalities from the deontic logic: obligations ${\mathcal {O}_{k}(a)[d]}$, prohibitions ${\mathcal {F}_{k}(a)[d]}$ and permissions ${\mathcal {P}_{k}(a)[d]}$. In all three cases the operator indicates the agent $k$, the action $a$, and the time constraint $d$ (the modality is in force within $d$ units of time). We can find the contract disjunction $\varphi _1\vee \varphi _2$, and contract conjunction $\varphi _1 \wedge \varphi _2$, sequential composition $\varphi _1;\varphi _2$, delay $\mathsf {wait}(d)$, the conditional contract $\text {cond}_{k}(a)[d](\varphi _1,\varphi _2)$, and the reparation operator $\varphi _1\blacktriangleright \varphi _2$. Finally, there is the possibility of repetition introduced by the variable $x\in \mathsf {fvars}$ and the recursion operator $\mathsf {rec\;}x.\varphi$. Using these basic contract combinators, we can define more complex ones, for example a prohibition which persists until a particular action is performed—a prohibition on agent k from performing action a until party l performs action b, written , and defined as follows:

In order to simplify the semantics of the language, we define a congruence in the language.

Definition 2

We define the relation as the least congruence relation that includes:

The operational semantics of the language is defined by the rules appearing in Figs. 1 and 2. The operational semantics of the contracts has three kind of transitions: (i) to denote that contract $\varphi$ can evolve (in one step) to $\varphi '$ when action a is performed, which involves party k (and possibly other parties); or (ii) indicating that the contract $\varphi$ can evolve to $\varphi '$ when the action a is not offered by any party other than k; or (iii) to represent that contract $\varphi$ can evolve to contract $\varphi '$ when d time units pass. We will use variable $\alpha$ to stand for a label of either form: (a, k) or $\overline{(a,k)}$. The rules of the operational semantics are always applied to irreducible terms.

Next, define the predicate $\mathsf {vio}(\varphi )$ that indicates if a contract is currently violated.

Definition 3

We say that an irreducible contract $\varphi$ is in a violated state, written $\mathsf {vio}(\varphi )$, if and only if the contract has already been violated:

We can now define how contracts evolve alongside a system, and what it means for a system to satisfy a contract.

Definition 4

Given a contract with alphabet $\mathsf {Act}'$ and a system $\mathcal{A}$, we define the semantics of $\varphi \Vert \mathcal{A}$—the combination of the system with the contract—with alphabet $\mathsf {Act}$ with $\mathsf {Act}'\subseteq \mathsf {Act}$ through the following rules:

Rule $\mathbf{M1}$ and $\mathbf{M2}$ handles synchronization between the contract and the system. If an action a performed by the system is of interest to the contract, the contract evolves alongside the system ($\mathbf{M1}$), if the contract allows an agent to perform an action but only agent k (and no other agent) is willing to engage in the action, then only the contract evolves ($\mathbf{M2}$). Rule $\mathbf{M3}$ handles actions on the system which the contract is not interested in. Finally, rule $\mathbf{M4}$ ensures that time cannot skip over a violation.

Definition 5

Let $\mathcal{A}$ be a system and be a contract.

• System $\mathcal{A}$ can break $\varphi$, written $\textsf {break}(\mathcal{A},\varphi )$, if there exists a computation that leads to a violation of the contract: for some $n\ge 0$ and contracts $\varphi _0$ till $\varphi _n$ such that:

  

  and .

• System $\mathcal{A}$ may fulfil $\varphi$, written $\textsf {fulfill}(\mathcal{A},\varphi )$, if there exists a computation of the system that fulfils the contract: for some $n\ge 0$ and contracts $\varphi _0$ till $\varphi _n$:

  

  and for $0\le k<n$, and $\varphi _n\equiv \top$.

Note that there are contracts which may never be fulfilled. An example of such a contract is $\varphi =\mathsf {rec\;}x. [a,k,\infty ](\bot ,\infty )$, which may never be fulfilled since there are no transitions from this contract leading to $\top$. Nevertheless, if agent k never performs action a, then neither is the contract broken.

Fig. 3.

Adaptation of the Madrid Barajas airport regulations

3 Case Study

The case study presented in this section (Fig. 3) is based on the Madrid Barajas airport regulations [1]. The contract describing our case study can be formalized using our contract calculus as follows:

$$\begin{aligned} \textit{PBS}\,::=\,&((\varphi _0\wedge \varphi _{10}\wedge \varphi _{15}); \varphi _1; \varphi _2; \varphi _3; \\ {}&(\varphi _5\wedge \varphi _6\wedge \varphi _7\wedge \varphi _8\wedge \varphi _9\wedge \varphi _{12}\wedge \varphi _{13}\wedge \varphi _{14}); \\ {}&(\varphi _4\wedge \varphi _{11}))\wedge \varphi _{16}\wedge \varphi _{17}) \end{aligned}$$

Where the formulas $\varphi _{1},\ldots ,\varphi _{17}$ are defined in Fig. 4 such that p, S, c refer to the passenger, the security airport staff, and the airline company, respectively; while $t_{0}$ is departure estimated time. Note that the clauses $\varphi _0$ to $\varphi _{17}$ are used to express the different parts of the contract, and combined in the top-level contract expression $\textit{PBS}$. The translation is quite straightforward although it is not automated. We have attach a formula to each point of the contract indicating where it has been formalized.

Fig. 4.

Madrid Barajas airport regulations formulae.

Then, this approach allows us to check and determine if any of the agents involved in the plane boarding system breaks the contract. In this case, our formalism allows us to determine, for instance, if it was the passenger who violated the contract and if so why, e.g. because she did not present her boarding pass within the specified time at the check-in desk, or because she was taking articles to the restricted security area.

4 Runtime Verification

The operational semantics we give to contracts provides us with a framework for contract monitoring: to monitor contract $\psi \in \mathcal{C}$, we start the monitor in state $\psi$ and update the state whenever the system performs an action according to the operational semantics. A violation is reached once the violation predicate is satisfied by the system. In the rest of this section, we concretely show how our logic can be automatically monitored using a derivative-based algorithm [4].

The idea behind derivative-based or term rewriting-based monitoring is that the formula still to be monitored is used as the state of the monitoring system. Whenever an event e is received with the system being in state $\psi$, the state is updated to $\psi '$ such that any trace of events es matches $\psi '$, if and only if $e\!:\!es$ (the trace starting with e, followed by es) matches $\psi$. This is repeated and a violation is reported when (and if) the monitoring state is reduced to a formula which matches the empty trace. In our contract logic, the operational semantics provide precisely this information, with $\psi '$ being chosen to be the (unique) formula such that² (where the monitoring systems observes the action a performed by party k), and $\mathsf {vio}(\psi )$ indicates whether $\psi$ matches the empty string (immediately violates the contract).

In timed logics, this approach has to be augmented with timeout events which, in the absence of a system event, still change the formula. For example, the contract $\mathsf {wait}(d);\varphi$ would evolve to $\varphi$ upon d time units elapsing. Similarly, if d time units elapse (with no system events received), we evolve the contract ${\mathcal {O}_{k}(a)[d]};\varphi$ to $\bot ;\varphi$, which is equivalent to $\bot$, thus enabling us to flag the violation as soon as it happens. If we were to wait for a system event, the violation might end up being identified too late. In our case, we use the timeout function to enable the setting of a timer to trigger the monitoring state update, evolving $\varphi$ to the unique formula $\varphi '$ according to the timed operational semantics . Also, system events carry a timestamp, through which the contract can be moved ahead in time upon receiving the event.

In order to formalise these ideas, we need a notion of structural equivalence. Intuitively, two contracts are structurally equivalent if they only differ in the time constraints and so they can perform the same actions.

Definition 6

Consider the relation $\mathcal{R}\subseteq \mathcal{C}\times \mathcal{C}$ defined as follows:

The structural equivalence congruence, denoted by $\equiv _s$ is the smallest congruence containing $\mathcal{R}$.

Proposition 1

Let be two structurally equivalent contracts, $\varphi \equiv _s\psi$. Then $\mathsf {vio}(\varphi )=\mathsf {vio}(\psi )$ and .

Proof

The proof follows using structural induction.

Definition 7

The timeout of a contract $\varphi$, written $\text {timeout}(\varphi )$, is inductively defined as follows:

Finally, we obtain the result that we need: any timed transition taking less than the timeout of a contract preserves the structure of a contract.

Proposition 2

Given contract $\varphi$ and time $t < \text {timeout}(\varphi )$, advancing $\varphi$ by t time units preserves the structure of the contract: if , then: $\varphi \equiv _s \varphi '$.

Proof

The proof is simple by structural induction.

We can now define the closure of a contract $\varphi$ as all formulae reachable from $\varphi$ through action transitions and timeout time transitions.

Definition 8

We define the closure of a contract formula $\varphi$, written $\textit{closure}(\varphi )$, to be the set of all contract formulae reachable through a combination of visible action transitions and timeout transitions. Formally, $\textit{closure}(\varphi )$ is the smallest set such that: (i) $\varphi \in \textit{closure}(\varphi )$; (ii) if $\varphi _1 \in \textit{closure}(\varphi )$, and , then $\varphi _2 \in \textit{closure}(\varphi )$; and (iii) if $\varphi _1 \in \textit{closure}(\varphi )$, and , then $\varphi _2 \in \textit{closure}(\varphi )$.

It is easy to prove, that for a contract $\varphi$ whose time constraints are non-zero constants, the closure of $\varphi$ does not exhibit Zeno-like behaviour³. It also follows that the relations of timeout time steps and visible event steps are sufficient to characterise the operational semantics progress of a contract to a violation or otherwise.

4.1 A Monitoring Algorithm

The monitoring algorithm for our contract logic is shown in Algorithm 1. The state of the monitor is stored in variable contract while variable systime keeps track of the last timestamp processed by the system. Initially, these variables are set to $\psi$ and 0 (line 1). The monitoring algorithm is effectively a loop (lines 2–17) which checks whether there was a violation upon every iteration. Upon entering the loop, any pending timer triggers are replaced (lines 3–5), enacting a process which creates a special timeout event (line 4) to be launched (asynchronously) after the current contract times out. In the meantime, execution is blocked until an event is received (line 6). If the event received is the timeout event, the monitored formula is updated accordingly using the timestep function which returns the unique formula satisfying with the time advanced by $\textit{timeout}(\psi )$ time units (lines 7–10). If, however, the event received is a system event e with timestamp t, the monitoring state is updated by first advancing time by $(t-\textit{systime})$ time units, and then stepping forward using the step function which returns the unique formula such that (lines 11–14). Finally, the systime variable is updated accordingly (line 16).

It is worth noting that the algorithm replicates the two types of transitions required to advance a contract: (i) maximally advancing time until the structure of the contract changes (the case of a timeout event); and (ii) processing a system event. This ensures that the state of the contract monitor advances steadily in correct steps (assuming that timestep and step correctly implement the rules from the semantics). Furthermore, progress is ensured since stepping along maximal time steps never results in Zeno-like behaviour.

5 Runtime Verification Using Larva

Rather than programming the runtime verification algorithm from scratch, we have built it on top of an existing runtime verification tool. We used Larva [6], which uses Dynamic Automata with Timers and Events (DATEs) as a specification language. DATEs are symbolic timed automata enriched in many aspects.

There are three main elements in DATE transitions: (i) Events refer to observable actions which a DATE may react to. (ii) Conditions are boolean expressions taking into consideration both the DATE’s symbolic state and the system state, which decides whether a transition is taken or not. (iii) Actions are modifications that are done to the DATE or system state upon observing an event and satisfying the condition. What follows formally defines these concepts.

Events which a DATE will be able to react to are either (i) system events over an alphabet $\textsc {SystemEvent}$, corresponding to control- or data-flow points of interest during the execution of the system; or (ii) timer events which are triggered upon a timer t reaching a threshold limit L written $t@L$. Timer limits can either take the form of a time constant $T \in \mathbb {T}$ (where $\mathbb {T}$ refers to the continuous time domain), or deadline variables $D \in \textsc {Deadline}$. Unlike constant limits, deadline variables can be dynamically modified during the traversal of the DATE.

$$\begin{aligned} \textsc {Event}::= \textsc {SystemEvent}\mid \textsc {Timer}@(\mathbb {T}\cup \textsc {Deadline}) \end{aligned}$$

DATE conditions and actions may also refer to the state of the system which is being monitored e.g. to react to a login event only if the system is in alert mode. The state of the system $\sigma$ will be assumed to range over the type $\textsc {State}_s$. Besides, monitors may keep their own state, e.g. the monitor may keep track of how many users are logged in, in order to react to a login only when more than 100 concurrent users are using the system. The symbolic DATE state $\mu$ will be assumed to range over the type $\textsc {State}_m$.

In addition, a DATE configuration will also keep track of the timer values $\tau \in \textsc {State}_T$, assigning a time value to each time such that $\textsc {State}_T= \textsc {Timer}\rightarrow \mathbb {T}$. Similarly, it keeps track of the current value of the timer variable deadlines $\delta \in \textsc {State}_D$ where $\textsc {State}_D= \textsc {Deadline}\rightarrow \mathbb {T}$. We will abuse notation and write $\delta (L)$ to extend the function to work also on constant deadlines (in which case that constant deadline is returned) and $\tau + \varDelta$ (where $\varDelta \in \mathbb {T}$) to denote the timer state in which all timers are advanced by $\varDelta$ time units. The symbolic state of a DATE is thus defined to be a combination of all these parts: $\textsc {State}_{M}^{+}= \textsc {State}_m\times \textsc {State}_T\times \textsc {State}_D$.

Conditions $c \in \textsc {Condition}$ are predicates over the system and full monitoring state:

$$\textsc {Condition}= (\textsc {State}_s\times \textsc {State}_{M}^{+}) \rightarrow \mathbb {B}$$

Similarly, actions $\alpha \in \textsc {Action}$ are functions which, based on the system state, may update any part of the full monitoring state:

$$\textsc {Action}= (\textsc {State}_s\times \textsc {State}_{M}^{+}) \rightarrow \textsc {State}_{M}^{+}$$

Formally Defining DATEs. A DATE is quadruple $\langle Q,q_0,K,B\rangle$ where Q is a finite set of states, $q_0 \in Q$ is the initial state, $K \subseteq (Q\times \textsc {Event}\times \textsc {Condition}\times \textsc {Action}\times Q)$ is a set of event-condition-action transitions, and $B \subseteq Q$ is a set of bad states. We will write $q \xrightarrow {e \mid c \mapsto \alpha } q'$ to denote a transition $(q,e,c,\alpha ,q') \in K$.

The following figure shows an example of a DATE whereupon the detection of a login event on alert mode, a timer of ten minutes is started. If the ten minutes elapse before a logout, the DATE reaches a bad state.

The event triggers from a DATE state q, written , are defined to be all events which appear on transitions outgoing from q: .

The semantics of a DATE with dynamic timer deadlines can now be defined using this notation. The configuration of the monitor consists of (i) the state $q \in Q$ of the DATE; and (ii) the symbolic monitoring state $\sigma \in \textsc {State}_{M}^{+}$ of the monitor. Given a monitoring configuration, the earliest timer trigger is the least time which will trigger an outgoing timer event transition if no other event is received:

The semantics of DATEs will specify how the configuration of the DATE changes upon event triggering or time passing. We will have two forms of operational semantics relations: (i) $C \xrightarrow {e, \varDelta , \sigma } C'$ to denote that the monitor moves from configuration C to $C'$ upon the system receiving event e after $\varDelta$ time units (from the last transition) and with the system state snapshot at that time being $\sigma$; (ii) to denote that the monitor goes from configuration C to $C'$ after $\varDelta$ time units of inactivity at the end of which the system state is $\sigma$.

The first relation is defined with the implicit condition that an event e has triggered and another two preconditions: the existence of a transition triggering on e and the satisfaction of the condition c. The side-condition ensures that no timer-triggered transitions should have modified the configuration before.

The second relation is similar to the previous but, while not requiring the occurrence of a system event, requires that the timer has reached its deadline.

Building on the earlier example, consider the case where the automaton is in the second state with the timer just reset: $(q_2,(\varnothing ,t\mapsto 0,t\mapsto 10))$. If a logout event occurs after six minutes, then $\varDelta =6$, while $\textit{earliest}(q_2,(\varnothing ,t\mapsto 6,t\mapsto 10)) = 10\,-\,6 = 4$. Therefore the first relation would apply, updating the configuration to $(q_1,(\varnothing ,t\mapsto 6,t\mapsto 10))$. On the other hand, if no logout event occurs within ten minutes, then $\textit{earliest}(q_2,(\varnothing ,t\mapsto 0,t\mapsto 10)) = 10-0 = 10$ causing the second relation to be applied resulting in the configuration $(q_\times ,(\varnothing ,t\mapsto 10, t\mapsto 10))$.

6 Implementation

The operational semantics given to the contracts, along with the timers and events, provide the framework to transform contracts in our calculus into DATEs which can be used to runtime verify the performance of parties involved. More details about the implementation can be found in [3] and in the Appendix.

We have adapted the derivative-based [4] runtime verification algorithm in order to obtain a DATE which reacts to the events appropriately. The resulting two-state DATE keeps track of the current contract in a variable $\varphi$ and updates triggers on either an event or the timeout triggers. Initially, $\varphi$ is set to the contract to monitor, while T to $\text {timeout}(\varphi )$:

s

The function $\textit{next}(\varphi ,e)$ corresponds to $\textit{step}(\textit{timestep}(\varphi , \varDelta t), e)$ while $\textit{next}_{\textit{time}}(\varphi )$ corresponds to $\textit{timestep}(\varphi , \varDelta t)$—in both cases $\varDelta t$ is the time elapsed since the last processed event. Using this construction, a trace leads to the bad state of the DATE if and only if it violates the initial contract. It is worth noting that since any computable function can be embedded as the action of a DATE transition, the translation is made possible by the computability of derivatives over time and event steps.

Practical Evaluation. To test our approach, we implemented the case study in Java with each action represented as a method call. When evaluated empirically, runtime verification tools, typically (e.g. [5]) get evaluated by comparing the time needed to run the system with and without monitoring. In this case, this is not practical since the system is simply a sequence of dummy method executions. Instead, the purpose of this quantitative evaluation is (i) to verify the correct behaviour of the monitor, i.e., that a violation is indeed reported when it actually occurs and vice versa; and (ii) to verify our intuition that the monitor will scale linearly with the size of the execution of the underlying system.

A number of test cases were generated, each representing the interactions of a single user involving a varying number of actions. In each case, the monitor verdict was as expected. Subsequently, different levels of traffic were generated by launching several users in parallel ranging from 100 to 100,000 users. The experiment⁴ was run on a laptop with an Intel i7-855U processor, 16 GB RAM.

Thousands of users	0.1	0.5	1	5	10	50	100
No monitoring (s)	0.0556	0.231	0.261	0.736	0.811	7.00	12.1
With monitoring (s)	0.104	0.433	0.595	2.16	4.05	18.1	38.4
Difference (s)	0.0480	0.202	0.334	1.43	3.24	11.1	26.4
Difference per user (ms)	0.480	0.404	0.334	0.285	0.324	0.223	0.264

The results in the table above show that as the number of users increases, the CPU time per user stabilises at around 0.3 ms. This confirms our reasoning that since the individual user monitors do not interact, the monitoring effort scales linearly to the number of users. One would only expect this trend to stop when reaching a large number of users such that the performance of an underlying framework starts deteriorating, e.g., the thread pool grows larger than what is efficiently manageable.

Regarding memory, since contract monitors only need to keep track of a state of bounded size per user per contract, this was not considered to be an issue.

7 Conclusions and Future Work

In this paper, we have presented a runtime verification algorithm for a real-time contract calculus, proved to be correct. Also, we presented an implementation of the algorithm as part of an established runtime verification tool Larva.

It is worth noting that despite the fact that there is much work on real-time deontic logics (see [2] for a summary and comparisons of such works), and limited work on monitoring of deontic logics (e.g. see [7, 8, 16]), the overlap between the two has been largely neglected.

There are various research directions this research opens. Regarding the runtime verification aspect, an interesting challenge is how we can use our techniques for runtime enforcement: starting from a specification, how we can synthesise algorithmic machinery to ensure that the system under scrutiny does not violate the specification, e.g. by delaying or injecting events. In particular, there is a body of work on runtime enforcement of timed properties, e.g. [9] which could offer insight on how our work can be extended to build contract enforcement engines, a notion that has not been widely explored in the deontic logic world.