Automated repair for timed systems

The analysis of system design models using model checking technology is an important step in the system design process. It enables the automated verification of system properties against given design models. The automated nature of model checking facilitates the integration of the verification step into the design process since it requires no further intervention of the designer once the model has been formulated and the property has been specified.

Often it is sufficient to abstract from real time aspects when checking system properties, in particular when the focus is on functional aspects of the system. However, in certain domains, non-functional properties of the system such as response times or the timing of periodic behavior play an important role. In such cases, it is necessary to incorporate real time aspects into the models and the specification, as well as to use specialized real-time model checking tools, such as UPPAAL [10], Kronos [44] or opaal [16] during the verification step.

Next to the automatic nature of model checking, the ability to return counterexamples, in real-time model checking often referred to as timed diagnostic traces (TDT), is a further practical benefit of the use of model checking technology. A TDT describes a timed sequence of steps that lead the design model from the initial state of the system into a state violating a real-time property. However, a TDT alone neither constitutes a causal explanation of the property violation, nor does it provide hints as to how to correct the model.

We present an automated method that computes proposals for possible repairs of a network of timed automata (NTA) that avoid the violation of a timed safety property. Consider the TDT depicted as a time annotated sequence diagram [9] in Fig. 1c. This scenario describes a simple message exchange where the process client sends a message req to the process db which, after some processing steps returns a message ser to client. Assume a requirement on the system stating that the time from sending req to receiving ser is not to be more than 4 time units. Further assume that the timing interval annotations on the sequence diagram represent the minimum and maximum time for the message transmission and processing steps that the NTA, from which the diagram has been derived, permits. It is then easy to see that it is possible to execute the system in such a way that this property is violated.

Network of timed automata—running example

Full size image

Various changes to the underlying NTA model depicted in Fig. 1 may avoid this property violation. We present analyses that can suggest a whole range of repairs in addition to clock bound variation, such as modifying clock bounds, comparison operators in constraints, clock references, clock resets, and location urgency. Examples of repairs computed for the model in Fig. 1 are:

• Reducing the maximum time it takes to transmit ser message to be at most 1 time unit by exchanging \(z<=2\) with \(z<=1\).

• Exchanging the comparison operator in the constraint \(w \ge 1\) to \(w<1\) ensures that the time to send a request is below 1 time unit.

• An exchange of clock z in \(z \le 2\) with clock y restricts the time of processing and receiving the response to at most 2 time units.

• To reset the clock y on the previous transition instead ensures that the time for sending and processing the request is below 1 time unit.

• Making the location serReceiving urgent reduces the time to receive a response to 0.

Proposing such changes to the model may either serve to correct clerical mistakes made during the editing of the model, or point to necessary changes in the dimensioning of its time resources, thus contributing to improved design space exploration.

The repair method described in this paper relies on an encoding of a TDT as a constraint system in linear real arithmetic. This encoding provides a symbolic abstract semantics for the TDT by constraining the sojourn time of the NTA in the locations visited along the trace. The constraint system is then augmented by auxiliary model variation variables which represent syntactic changes to the NTA model, for instance, the variation of a location invariant condition or a transition guard. We assert that the thus modified constraint system implies the non-reachability of a violation. At the same time, we assert that the model variation variables have a value that implies that no change of the NTA model will occur, for instance, by setting a clock bound variation variable to 0. This renders the resulting constraint system unsatisfiable.

In order to compute a repair, we derive a partial MaxSMT instance by turning the constraints that disable any repair into soft constraints. We solve this MaxSMT instance using the SMT solver Z3 [18]. If the MaxSMT instance admits a solution, the resulting model provides values of the model variation variables. These values indicate a repair of the NTA model which entails that along the sequence of locations represented by the TDT, the property violation will no longer be reachable.

In a next step it is necessary to check whether the computed repair is an admissible repair in the context of the full NTA. This is important since the repair was computed locally with respect to only a single given TDT. Thus, it is necessary to define a notion of admissibility that is reasonable and helpful in this setting. To this end, we propose the notion of functional equivalence which states that as a result of the computed repair, neither erstwhile existing functional behavior will be eliminated, nor will new functional behavior be added. Functional behavior in this sense is represented by the languages accepted by the untimed automata of the unrepaired and the repaired NTAs. Functional equivalence is then defined as equivalence of the languages accepted by these automata. We propose a zone-based automaton construction for implementing the functional equivalence test that is efficient in practice.

We have implemented our proposed method in a proof-of-concept tool called TarTar. Our evaluation of TarTar is based on several non-trivial NTA models taken from the literature, including the frequently considered pacemaker model [29]. For each model, we automatically generated mutants by injecting syntactic modifications which we then model checked using UPPAAL and repaired using TarTar. The evaluation shows that our technique is able to compute an admissible repair 69–\(88\%\) of the detected faults.

1.1 Related work

There are relatively few results available on a formal treatment of TDTs. The zone-based approach to real-time model checking, which relies on a constraint-based abstraction of the state space, is proposed in [23]. The use of constraint solving to perform reachability analysis for NTAs is described in [45]. This approach ultimately lead to the on-the-fly reachability analysis algorithm used in UPPAAL [12]. Henning et al. [17] defines the notion of a time-concrete UPPAAL counterexample. Work documented in [40] describes the computation of concrete delays for symbolic TDTs. The above cited approaches address neither fault analysis nor repair for TDTs. Our use of MaxSMT solvers for computing minimal repairs is inspired by the use MaxSAT solvers for fault localization in C programs, which was first explored in the BugAssist tool [28]. We present an approach that uses a counterexample to prevent bad behavior while the technique in [11] computes repairs to ensure missing expected behavior. The algorithm presented in [19] repairs a TA by adding time constraints, whereas the approach in this paper modifies existing time constraints. Our approach also shares some similarities with syntax-guided synthesis [2, 41], which has also been deployed in the context of program repair [35]. One key difference is how we determine the admissibility of a repair in the overall system, which takes advantage of the semantic restrictions imposed by timed automata. The modification of time constraints by extra variables can also be interpreted as a parametric timed automata (PTA). A PTA is used in [1] to repair a TA that does not behave according to an oracle. Each of the generated repairs can only prevent a finite number of explicit timed traces whereas the repairs generated by our approach can prevent an infinite number of symbolically encoded traces. The algorithm in [22] checks whether a synthesized TA exists for a given set of properties. If this automaton does not exist, mixed integer linear programming is used to modify bounds in the specified properties such that a TA can be synthesized. The modifications of bounds in STL specifications is a different goal than the modification of bounds in the TA that we propose.

1.2 Contributions

We augment in this work the original publications in [31] and [32] on computing syntactic repairs for timed systems. More examples in this work illustrate the approach. We also added proofs for the theorems, extended the definitions given in the preliminaries and harmonized the presentation.

1.3 Structure of the paper

We will introduce the automata and real-time concepts needed in our analysis in Sect. 2. In Sect. 3, we present the logical formalization of TDTs. The repair and admissibility analyses are presented in Sect. 4 and 5, respectively. We present the implementation in the tool TarTar in Sect. 6. In Sect. 7, we report on experimental evaluation and case studies. We provide a conclusion and perspectives for future research in Sect. 8.

The timed automaton model that we use in this paper is adapted from [12]. Given a set of clocks C, we denote by \({{\mathcal {B}}}(C)\) the set of all clock constraints over C, which are conjunctions of atomic clock constraints of the form \(c \sim n\), where \(c \in C\), \(\sim \in \{<,\le , =, \ge , >\}\) and \(n \in {\mathbb {N}}\). For the remainder of this section, we fix a finite set of clocks C.

Definition 1

(Timed Automaton (TA) [12]) A Timed Automaton T is a tuple \(T = (L, l^0, \varSigma , \varTheta , I)\) where L is a finite set of locations, \(l^0 \in L\) is an initial location, \(\varSigma\) is a finite set of actions, \(\varTheta \subseteq L \times {{\mathcal {B}}}(C) \times \varSigma \times 2^C \times L\) is the transition relation, and \(I: L \rightarrow {{\mathcal {B}}}(C)\) denotes a labeling of locations with clock constraints, referred to as location invariants. For \(\theta \in \varTheta\) with \(\theta = (l, g, a, r, l')\), we refer to g as the guard of \(\theta\) and to r as its clock resets.

The operational semantics of T is given by a timed transition system (TTS) in Definition 2. A clock valuation u is a function \(C \rightarrow {\mathbb {R}}_{\ge 0}\). For a clock constraint b, we write \(u \models b\) iff b evaluates to true in u. There are two types of transitions. An action transition models the execution of an action whose guard is satisfied. These transitions are instantaneous and reset the specified clocks. The passing of time in a location is modeled by delay transitions. Both types of transitions guarantee that location invariants are satisfied in the pre and post state.

Definition 2

(Timed Transition System (TTS) [6]) For a Timed Automaton \((L, l^0, \varSigma , \varTheta , I)\), a timed transition system is a tuple \(H=(S, s_0, \varSigma , \rightarrow )\) where \(S=\{(l, u) \in L\times {{\mathcal {R}}}^C_{\ge 0}\mid u\models I(l)\}\), \(s_0\) is the initial state \((l^0, u_0)\) such that \(u_0\) maps all clocks to 0, and a transition \((l, u) {\mathop {\longrightarrow }\limits ^{t}} (l', u')\) is in \(\rightarrow\) iff

• (action transition) \(t = (l, g, a, r, l') \in \varTheta\), \(u \models I(l) \wedge g\), \(u' \models I(l')\) and for all clocks \(c \in C\), \(u'(c) = 0\) if \(c \in r\) and \(u'(c) = u(c)\) otherwise; or

• (delay transition) \(t \in {\mathbb {R}}_{\ge 0}\), \(l=l'\), \(u \models I(l)\), \(u' \models I(l)\) and \(u' = u + t\).

An urgent location is a location that has to be left again without taking a delay transition [6]. Urgent locations are syntactic sugar of Uppaal and can be expressed as an additional clock p which is reset with entering the location and a location invariant \(p=0\).

A run [12] of a TTS with initial state \(s_0\) is a sequence of states and actions of the form \(s_0\xrightarrow {t_1}\xrightarrow {a_1}s_1 \xrightarrow {t_2}\xrightarrow {a_2}\ldots\) with \(s_i=(l_i, u_i)\) where every \(t_i\) is in \({\mathbb {R}}_{\ge 0}\) with \((l_i,u_i)\xrightarrow {t_i}(l_i,u_{i+1})\) in \(\rightarrow\) , and every \(a_i\) is in \(\varSigma\) with \((l_i,u_{i+1})\xrightarrow {(l_i,g,a_i,r,l_{i+1})}(l_{i+1},u_{i+1})\) in \(\rightarrow\). A timed trace [12] is a sequence of timed actions \(\xi = (t'_1, a_1), (t'_2, a_2), \ldots\) that is generated by a run of a TTS associated with a TA, where \(t'_i=\sum \limits _{0< j \le i} {t_{j}}\). We capture families of timed traces that perform the same sequence of action transitions but differ in their delay transitions by the notion of a symbolic timed trace.

Definition 3

(Symbolic Timed Trace (STT)) A symbolic timed trace (STT) of T is a sequence of actions Y\(= \theta _0,\dots ,\) \(\theta _{n-1}\). A realization of Y is a sequence of delay values \(\delta _0,\dots ,\delta _{n}\) such that there exists states \(s_0,\dots ,s_n,s_{n+1}\) with \(s_i {\mathop {\longrightarrow }\limits ^{\delta _{i}}} {\mathop {\longrightarrow }\limits ^{\theta _{i}}} s_{i+1}\) for all \(i \in [0,n)\) and \(s_n {\mathop {\longrightarrow }\limits ^{\delta _{n}}} s_{n+1}\). We say that a STT is feasible if it has at least one realization.

The timed language for a TA T is the set of all its timed traces, which we denote by \({{\mathcal {L}}}_T(T)\). The untimed language of T consists of words over T’s alphabet \(\varSigma\) so that there exists at least one timed trace of T forming this word. Formally, for a timed trace \(\xi = (t_1, a_1),(t_2, a_2)\ldots\) , the untime operator \(\mu (\xi )\) returns an untimed trace \(\xi _{\mu } = a_1 a_2 ...\) . We define the untimed language \({{\mathcal {L}}}_{\mu }(T)\) of the TA T as \({{\mathcal {L}}}_{\mu }(T) = \{ \mu (\xi ) \mid \xi \in {{\mathcal {L}}}_T(T) \}\). We represent a finite untimed language using a Nondeterministic Finite Automaton and an infinite untimed language using a Nondeterministic Büchi Automaton.

Definition 4

(Nondetermistic Finite Automaton (NFA) [6]) A nondeterministic finite automaton is a tuple \(M = (S, \varSigma , \rightarrow , S_0,F)\) where S denotes a finite set of states, \(\varSigma\) denotes an alphabet, \(\rightarrow \subseteq S \times \varSigma \times S\) denotes a transition relation, \(S_0 \subseteq S\) denotes the set of initial states, and \(F \subseteq S\) denotes the set of acceptance states. We write \(s {\mathop {\longrightarrow }\limits ^{a}} s'\) when \((s, a, s') \in \rightarrow\). An execution of M is a sequence \(s_0 {\mathop {\longrightarrow }\limits ^{a_0}} s_1\ \ldots {\mathop {\longrightarrow }\limits ^{a_{n-1}}} s_n\) such that \(s_0 \in S_0\) and \(s_n \in F\). A run \(s_0, s_1, \ldots , s_n\) of M is the projection of an execution \(s_0 {\mathop {\longrightarrow }\limits ^{a_0}} s_1 \ldots {\mathop {\longrightarrow }\limits ^{a_{n-1}}} s_n\) on the state sequence. M accepts a word \(w = a_0, a_1, \ldots , a_{n-1}\) when an execution \(s_0 {\mathop {\longrightarrow }\limits ^{a_0}} s_1 \ldots {\mathop {\longrightarrow }\limits ^{a_{n-1}}} s_n\) exists. The language \({{\mathcal {L}}}_f(M)\) recognized by M is the set of (finite length) words accepted by M.

Definition 5

(Nondeterministic Büchi Automaton (NBA) [6]) An NFA \(B = (S, \varSigma ,\rightarrow , S_0,F)\) is called a Büchi automaton in case it is used with an acceptance condition for infinite input sequences. For an infinite sequence r of states, let \(\text {inf}(r)=\{s \in S \mid r_i=s \; \text {for infinitely many} \; i\}\). An NBA B accepts an infinite word \(w = a_1 a_2 \ldots\), \(w \in \varSigma ^{\omega }\), iff B has an infinite run \(r=s_0s_1\ldots\) of states on w such that \(s_0 \in S_0\), \(\text {inf} (r)\cap F\not =\emptyset\) and \(\forall i\in {\mathbb {N}}^+_0,(s_i, a_{i+1}, s_{i+1}) \in \rightarrow\). The language \({{\mathcal {L}}}(B) \subseteq \varSigma ^{\omega }\) recognized by an NBA B is the set of infinite words accepted by B. \(\text {pref}({{\mathcal {L}}}(B))\) denotes the set of all finite prefixes of words in \({{\mathcal {L}}}(B)\).

For a given NFA or NBA M, the closure \(\textit{cl}(M)\) denotes the automaton obtained from M by turning every state into an accepting state. We call M closed iff \(M=\textit{cl}(M)\). Notice that an NBA accepts a safety language if and only if it is closed [5].

We use zones as given in Definition 6 in order to abstract an infinite-state TTS into a finite-state Zone Automaton, c.f. Definition 7.

Definition 6

(Zone [6]) A diagonal constraint is an extended clock constraint of the form \(x-y\sim n\) with two clocks x and y. For a finite set C of clocks, let \(\llbracket \varphi \rrbracket _C = \{ u \in {\mathbb {R}}^C_{\ge 0}\ |\ u\models \varphi \}\) denote the set of clock evaluations u satisfying a conjunction \(\varphi\) of diagonal clock constraints. A subset \(z \subseteq {\mathbb {R}}^C_{\ge 0}\) is called a zone if there exists \(\varphi\) for which \(z = \llbracket \varphi \rrbracket _C\).

Definition 7

(Zone Automaton (adapted from [6])) Assume a Timed Automaton \(T= (L, l^0, \varSigma , \varTheta , I)\). We define the zone automaton \(\llbracket T\rrbracket _Z = (S_Z, s_Z^0, \varSigma _Z , \varTheta _Z)\) for T such that \(S_Z = \{ (l , z) \mid l \in L, z\subseteq {\mathbb {R}}^C_{\ge 0}\text { is a zone}\}\), \(s_Z^0 = (l^0, \{u_0\})\), \(\varSigma _Z = \varSigma \cup \{\delta \}\) and a transition relation \(\varTheta _Z \subseteq S_Z \times \varSigma _Z\times S_Z\). Let \(z^\uparrow = \{u+d\mid u\in z, d\in \, \mathsf{R}\,^+_0\}\), and let z[r] denote the clock reset for a clock set r in a zone z such that in the resulting zone every clock in r evaluates to 0. We write \(l \overset{a}{\leadsto } l'\) for a transition \((l, a, l')\in \varTheta _Z\). The transition relation \(\varTheta _Z\) is the smallest relation that satisfies the following rules:

1. 1.

   If \((l, z) \in S_Z\), then \({(l, z)\overset{\delta }{\leadsto } (l, z^\uparrow \cap \llbracket I(l)\rrbracket _C)}\).

2. 2.

   If \({l\xrightarrow {\varphi ,a,r}l'\in \varTheta }\), then \({(l, z) \overset{a}{\leadsto }(l', (z \cap \llbracket \varphi \rrbracket _C)[r] \cap \llbracket I(l')\rrbracket _C)}\).

A trace \(a_0\ldots a_n\) is a trace of \(\varTheta _Z\) iff for \(0\le i\le n\), \(l_i \overset{a_i}{\leadsto } l_{i+1}\) exists and \(l_0 = l^0\). We call a trace of \(\varTheta _Z\) a symbolic trace.

\({{\mathcal {L}}}_T(\llbracket T \rrbracket _Z)\) denotes the set of timed traces with time delays that satisfy the zones of at least one symbolic trace of \(\llbracket T \rrbracket _Z\).

2.1 Property specification

We focus on the analysis of timed safety properties, which we characterize by an invariant formula that has to hold for all reachable states of a TA. These properties state, for instance, that there are certain locations in which the value of a clock variable is not above, equal to or below a certain (integer) bound. Formally, let \(T = (L, l^0, C, \varSigma , \varTheta , I)\) be a TA. A timed safety property \(\varPi\) is a Boolean combination of atomic clock constraints and location predicates @l where \(l \in L\). A location predicate @l holds in a state \((l', u)\) of T iff \(l'=l\). We say that an STT Y witnesses a violation of \(\varPi\) in T if there exists a realization of Y whose induced final state does not satisfy \(\varPi\). We refer to such an STT as a timed diagnostic trace (TDT) of T for \(\varPi\).

T satisfies \(\varPi\) iff all its reachable states satisfy \(\varPi\). This problem can be decided using model checking tools such as Kronos [44] and UPPAAL [10]. UPPAAL in particular computes a finite abstraction of the state space of an NTA using zones for the graph construction. Reachability analysis is then performed by an on-the-fly search of the zone graph. If the property is violated, the tool generates a feasible TDT that witnesses the violation. The objective of our work is to analyze TDTs and to propose repairs for the property violation that they represent. We use TDTs generated by the UPPAAL tool in our implementation, but we maintain that our results can be adapted to any other tool producing TDTs.

We further note that UPPAAL takes a network of timed automata (NTA) as input, which is a CCS [38] style parallel composition of timed automata \(T_1 \mid \ldots \mid T_n\), yielding a TA. Since our analysis and repair techniques focus on timing-related errors rather than synchronization errors, we use TAs rather than NTAs in our formalization. However, our repair analysis can be directly applied to the TA obtained by the parallel composition and the implementation in TarTar works directly on NTAs.

Example 1

The running example that we use throughout the paper consists of an NTA containing two timed automata, depicted in Fig. 1. As alluded to in the introduction, the TAs client and db synchronize via the exchange of messages modeled by the pairs of send and receive actions req! and req? as well as ser! and ser?, respectively. The transmission time of the req message is controlled by the clock variable w and can range between 1 and 2 time units. This is achieved by the location invariant \(\texttt {w<=2}\) on the reqReceived location in db together with the transition guard \(\texttt {w>=1}\) on the transition from reqReceived to reqProcessing. A similar mechanism using clock variable z is used to constrain the timing of the transfer of message ser to be within 1 and 2 time units. The processing time in db is constrained to exactly 1 time unit by the location invariant \(\texttt {y<=1}\) and the transition guard \(\texttt {y>=1}\). In client, a transition to location timeout can be triggered when the guard z==2 is satisfied in location serReceiving. The clock variable x, which is not reset until the next req message is sent, is recording the time that has elapsed since sending req and is used in location serReceiving in order to verify if more than 4 time units have passed since req was sent. Every transition in the system is labeled with an action \(\tau\). The timed safety property that we will consider for our example is \(\varPi = \lnot \mathtt {@client.serReceiving} \vee (x \le 4).\) For the violation of this property, UPPAAL produces the TDT \(S = \theta _0 \ldots \theta _3\) where

We present a logical formalization of the concept of Timed Diagnostic Traces (TDTs) generated by a real-time model checking tool. Practical model checking tools generate these traces in a textual format. In the case of UPPAAL, which we use for generating the traces used in the analysis in this paper, symbolic TDTs are stored in an XML formatted file. The formalization that we develop will enable a logic encoding and automated analysis of TDTs.

3.1 Timed diagnostic trace (TDT)

A TDT is a linear data structure that represents steps from an initial state of the system leading into a property violating state of an NTA. Given an NTA N and property \(\varPi\) this means that the final state in the TDT is violating \(\varPi\). Figure 2 represents an excerpt of a TDT obtained from the UPPAAL tool and illustrates the violation of the property \(\varPi = \lnot \mathtt {@client.serReceiving} \vee (x < 4)\) by the NTA in Fig. 1.

The TDT contains information regarding the locations, location invariants, transition guards and reset operations affected by the execution of transitions. It also contains a representation of the difference bound matrices (DBMs) that are attached to every location in the NTA. The TDTs that we consider are symbolic in the sense that they do not give concrete time values at which certain locations are reached, but rather constraints on the clock values that need to be met for the property violating state to be reachable. For instance, consider the DBM table entry \(\texttt {<clockbound clock1="sys.x"}\) clock2="sys.t(0)" bound="5" \(\texttt {comp="<="/>}\) in Fig. 2 which represents the constraint on x in the state serReceiving as \(x \le 5\). In other words, no concrete value of x when entering the violating state is given.

Excerpt from the XML representation of a symbolic TDT generated by UPPAAL

Full size image

The objective of our analysis is to identify possible syntactic changes to the NTA model in order to propose repairs for the violation of timed reachability properties. The symbolic representation of the valid clock assignments per location in the TDT given by DBMs, as is done for instance by UPPAAL, is not useful for this purpose. This is due to the fact that DBMs perform operations and optimizations on the constraints when they construct zones [12]. As a result, bound values in the UPPAAL code can not necessarily be directly associated with bound entries in the DBM. It is therefore necessary to define our own logic representation of the TDT. This representation is based on the following observations:

• The TDT represents an equivalence class of runs of the NTA in the sense that all runs in this class traverse the same sequence of action transitions. This yieds a sequence \(l_0...l_n\) of NTA locations that are reached during the execution of the TDT.

• For every location \(l_j\), there is a corresponding sojourn time in this location that we denote using a positive real valued delay variable \(\delta _j\).

• The value of every clock variable c in location \(l_j\), which we denote by \(c_{j}\), is constrained by the value of \(c_{j}\) when entering the location plus the delay \(\delta _j\) and any location invariant constraint that refers to c in location \(l_j\). Notice that we need to be able to refer to the values of clocks in individual location, which is why we choose a Static Single Assignment form encoding of the clock variables.

• For any clock c in the successor location \(l_{j+1}\), the value \(c_{j+1}\) is determined by the value \(c_{j}\) plus the sojourn time \(\delta _j\), if the clock is not being reset during the transition from \(l_j\) to \(l_{j+1}\), or 0 otherwise.

• The sojourn time \(\delta _j\) in a location \(l_j\) is constrained by the clock invariant conditions of the NTA component TAs that perform the computation step triggering the transition into location \(l_{j+1}\). This means that the clock value \(c_{j}\) plus \(\delta _j\) are bounded by any clock constraint that refers to a clock variable c. For instance, in the TDT in Fig. 2, the location \(\text {LocVec4}\) contains the TA location reqProcessing with the invariant \(\texttt {y <= 1}\). Hence, the sojourn time in \(\text {LocVec4}\) is constrained by \(y_4 + \delta _4 \le 1\).

• The transition from location \(l_j\) to location \(l_{j+1}\) is guarded by clock constraints on some of the clocks c, if at least one is given, and otherwise by true. This means that the time when entering location \(l_j\) as well as the time elapsing while in location \(l_j\) are constrained by these guards. We represent this by adding constraints of the form \(c_{j} + \delta _j \sim \beta\) with \(\beta \in {\mathbb {N}}\) to the symbolic constraint system. Notice that only the transition guards of the component TAs that performed the step leading to the step in the TDT need to be taken into account. In case the step performs a synchronization, the conjunctions of the transition guards for all clock variables on the sending and the receiving transitions need to be considered. To illustrate this point consider the \(\texttt {<transition from="State4" to="State5"}\) \(\texttt {edges="client.Edge3 db.Edge3"/>}\) entry in the TDT in Fig. 2 which specifies that both the client and db component TAs are executing a step. The synchronization is indicated by the \(\texttt {<sync>ser!</sync>}\) and \(\texttt {<sync>ser?</sync>}\) entries which refer to edges in the transition graph of the TAs engaged in this synchronous communication step. The \(\texttt {<guard>1</guard>}\) and \(\texttt {<guard>y>= 1</guard>}\) entries in these edges imply that this transition needs to be guarded by the condition \(true \wedge y \ge 1\), where the true corresponds to the transition guard in the client TA and \(y \ge 1\) is the guard in the db TA.

• When a location \(l_j\) is labeled as urgent, \(l_j\) has to be left immediately and we constrain the delay \(\delta _j\) in this location to have value 0.

3.2 TDT formalization

Our analysis relies on a logical encoding of TDTs in the theory of quantifier-free linear real arithmetic. For the remainder of this paper, we fix a TA \(T = (L, l^0, C, \varSigma , \varTheta , I)\) with a safety property \(\varPi\) and assume that Y\(=\theta _0,\dots ,\theta _{n-1}\) is an STT of T. We use the following notation for our logical encoding where \(j \in [0,n+1]\) is a position in a realization of Y and \(c \in C\) is a clock:

• \(l_j\) denotes the location of the pre state of \(\theta _j\) for \(j < n\) and the location of the post state of \(\theta _{j-1}\) for \(j=n\).

• \(c_{j}\) denotes the value of clock variable c when reaching the state at position j.

• \(\delta _j\) denotes the delay of the delay transition leaving the state at position \(j \le n\).

• \({\textit{reset}}_j\) denotes the set of clock variables that are being reset by action \(\theta _j\) for \(j < n\).

• \({\textit{ibounds}}(c,l)\) denotes the set of pairs \((\beta , \sim )\) such that the atomic clock constraint \(c \sim \beta\) appears in the location invariant I(l).

• \({\textit{gbounds}}(c,\theta )\) denotes the set of pairs \((\beta , \sim )\) such that the atomic clock constraint \(c \sim \beta\) appears in the guard of action \(\theta\).

• \({\textit{urgent}}\) denotes the set of indices of those locations \(l_j\), \(1 \le j \le n\), which are marked as urgent in the TA model from which Y has been derived.

To illustrate the use of \({\textit{ibounds}}\), assume location l to be labeled with invariants \(x > 2 \wedge x \le 4 \wedge y \le 1\), then \({\textit{ibounds}}(x,l) = \{(2, >), (4, \le )\}.\) The usage of \({\textit{gbounds}}\) is accordingly.

Definition 8

The timed diagnostic trace constraint system (TDTCS) associated with STT Y is the conjunction \(\mathcal {T}\) of the following constraints:

Let further \({\varPhi } \equiv \varPi [{{\textbf {c}}}_{n+1}/{{\textbf {c}}}]\) where \(\varPi [{{\textbf {c}}}_{n+1}/{{\textbf {c}}}]\) is obtained from \(\varPi\) by substituting every occurrence of a clock \(c \in C\) by \(c_{n+1}\). For instance, for the property \(\varPi\) used in Example 1 we have \({\varPhi } = \lnot @{client.serReceiving}\vee x_5 < 4\). Then, the \(\varPi\)-extended TDTCS associated with Y is defined as \(\mathcal {T}^\varPi = \mathcal {T} \wedge \lnot \varPhi\).

A satisfying assignment of a TDTCS \({{{\mathcal {T}}}}\) is a variable assignment to every clock \(c_j\) and delay variable \(\delta _j\) in \({{{\mathcal {T}}}}\) that satisfies every constraint in \({{{\mathcal {T}}}}\). A satisfying assignment of \({{{\mathcal {T}}}}\) induces a realization \(\delta _0...\delta _n\) of Y. \({{{\mathcal {T}}}}\) is a correct formalization of Y when any assignment of \({{{\mathcal {T}}}}\) contains a realization of Y and any realization r in Y is part of an assignment of \({{{\mathcal {T}}}}\).

Theorem 1

When a TDTCS \({{{\mathcal {T}}}}\) is created for an STT Y by Definition 8, then \(\delta ^c_0, \ldots ,\delta ^c_n\) is a realization of Y iff there exists a satisfying variable assignment \(\iota\) for \({{{\mathcal {T}}}}\) such that for all \(j\in [0,n],\iota (\delta _j) =\delta ^c_j\).

Proof

Assume an STT \(Y=\theta _0, ...., \theta _{n-1}\) of a TA, a TDTCS \({{{\mathcal {T}}}}\) of Y and an arbitrary delay sequence \(\delta =\delta _0, \ldots ,\delta _n\). We need to prove that \(\delta\) either satisfies Y and \({{{\mathcal {T}}}}\) or none of both. We show by induction over the delays that after each delay \(\delta _j\) the clocks values are equivalent in Y and \({{{\mathcal {T}}}}\), and satisfy the same clock constraints.

Base Case: In the initial state, no delay has yet occurred. The value of every clock in Y is 0, which is also ensured in \({{{\mathcal {T}}}}\) by \({{\mathcal {C}}}_0\).

Induction Step: It holds that the clock values in Y and \({{{\mathcal {T}}}}\) are equivalent for \(\delta _0...\delta _{j-1}\). We assume that after a time delay \(\delta _j\) a transition \(\theta _j\) transits from a location \(l_j\) to a location \(l_{j+1}\). A constraint in Y or \({{{\mathcal {T}}}}\) is not satisfied for \(\delta _j\) in one of the following cases:

• When \(\delta _j\) is negative, it violates the semantics of Y but also violates the constraints in \({{\mathcal {A}}}\) of \({{{\mathcal {T}}}}\).

• After \(\delta _j\), a guard \(c_i\sim \beta\) of a clock \(c_i\) is not enabled. The clock value of \(c_i\) was equivalent by assumption in Y and \({{{\mathcal {T}}}}\) before \(\delta _j\), and so is equivalent after \(\delta _j\). Since the guard is by construction of \({{{\mathcal {T}}}}\) encoded in Y and \({{{\mathcal {T}}}}\) and the clock value of \(c_i\) is equivalent, the guard is not enabled in Y and \({{{\mathcal {T}}}}\).

• After \(\delta _j\), a clock \(c_i\) does not satisfy a location invariant \(c_i\sim \beta\) in \(l_j\). Since the invariant is by construction encoded in Y and \({{{\mathcal {T}}}}\) and the clock value of \(c_i\) is equivalent as shown above, \(c_i+\delta _j\) is violated in Y and \({{{\mathcal {T}}}}\).

• A clock \(c_i\) does not satisfy a location invariant \(c_i\sim \beta\) in \(l_{j+1}\). By construction of \({{{\mathcal {T}}}}\), the invariant is encoded in Y and \({{{\mathcal {T}}}}\). The clock value of \(c_i\) is either \(c_i+\delta _j\) when \(c_i\) is reset or 0. By the construction of \({{{\mathcal {T}}}}\), \(c_i\) is reset in \({{{\mathcal {T}}}}\) exactly when it is reset by \(\theta _j\) in Y. Thus, \(c_i\sim \beta\) in \(l_{j+1}\) is not satisfied in Y and \({{{\mathcal {T}}}}\).

• \(\delta _j\) is not 0 even \(l_j\) is an urgent location. By construction of \({{{\mathcal {T}}}}\), \(l_j\) is in \({{\mathcal {U}}}\) and so only \(\delta _j=0\) is an assignment of \({{{\mathcal {T}}}}\). Thus, Y and \({{{\mathcal {T}}}}\) are not satisfied.

• With any other value of \(\delta _j\), the time constraints in Y and \({{{\mathcal {T}}}}\) are satisfied.

As we see, the clock values in Y and \({{{\mathcal {T}}}}\) are equivalent after each delay, and also equivalently satisfy the clock constraints in Y and \({{{\mathcal {T}}}}\). In consequence, \(\delta\) satisfies Y and \({{{\mathcal {T}}}}\), or none of both. \(\square\)

Theorem 1 ensures that an assignment of \({{{\mathcal {T}}}}\) and the contained realization of Y satisfy the same time constraints and location predicates. Consequently, they also equivalently violate or satisfy the time constraints and location predicates of which an invariant property \(\varPi\) exists. This allows us to infer Corollary 1 because the conjunction of \({{{\mathcal {T}}}}\) and \(\varPi\) is a \(\varPi\)-extended TDTCS \(\mathcal {T}^\varPi\). A modification of \(\mathcal {T}^\varPi\) that turns the formula unsatisfiable is also a potential repair in the underlying TA since it prevents the property violation. We will use this insight in the next section to compute a repair.

Corollary 1

An STT Y witnesses a violation of \(\varPi\) in a TA iff \(\mathcal {T}^\varPi\) is satisfiable.

Proof

We know by Theorem 1 that a realization r of an STT exists iff a satisfying assignment \(\iota\) of the STT exists. r and \(\iota\) satisfy equivalent location predicates and clock constraints and, thus, r and \(\iota\) equivalently hold or violate \(\varPi\). \(\square\)

We propose a repair technique that analyzes the responsibility of syntactic elements occurring in a single TDT for causing the violation of a specification \(\varPi\). We first present the formalization of different syntactic modifications of a TDT that can potentially remedy causes for property violations and then present the algorithm to compute a set of such syntactic modifications that are possible repairs. The question of admissibility of the computed repairs will be addressed in Sect. 5. Throughout this section, we assume that Y is a TDT for T and \(\varPi\).

4.1 Formal modification of syntactic elements

We introduce variation variables \(\textit{v}\) that represent correction values of syntactic elements of the TA for which Y is produced and which characterize the proposed repair. For instance, to modify clock bounds for a transition in a TA, a fresh variation variable is added to every clock bound occurring in location invariants and transition guards involved in this transition. The values of the variation variables are computed so that none of the realizations of Y in the modified automaton leads to a violation of \(\varPi\). This is done by defining a new constraint system that captures the conditions on the variable \(\textit{v}\) under which the violation of \(\varPi\) will not occur in the corresponding trace of the modified automaton. Using this constraint system, we then define a MaxSMT problem so that its solution minimizes the number of changes to T that are needed to achieve the repair.

4.1.1 Clock bound variation

Recall that the clock bounds occurring in location invariants and in transition guards are represented by the \({{\mathcal {I}}}\) and \({{\mathcal {G}}}\) sets defined for the TDT Y. We then introduce bound variation variables \(\textit{v}^{bv}_{i}\) describing the possible static variation in the TA code for a clock bound \(\beta\) with an index i in the set \(\text {ibounds} \cup \text {gbounds}\), and modify the TDT constraint system accordingly. A variation of the bounds only affects the location invariant constraints \({{\mathcal {I}}}\) and the transition guard constraints \({{\mathcal {G}}}\). We thus define an appropriate invariant variation constraint \({{{\mathcal {I}}}^{{\textit{bv}}}}\) and guard variation constraint \({{{\mathcal {G}}}^{{\textit{bv}}}}\) that capture the clock bound modifications:

We also need constraints ensuring that the modified clock bounds remain positive:

Putting all of this together, we obtain the bound variation TDT constraint system

which captures all realizations of Y in TAs \(T^{{\textit{bv}}}\) that are obtained from T by modifying the clock bounds by some syntactically consistent variations \(\textit{v}^{bv}_i\).

As an example, consider the bound variation for the guard \(y\ge 1\) of transition \(\varTheta _3\) in Example 1. The modified guard constraint, a conjunct in \({{{\mathcal {G}}}^{{\textit{bv}}}}\), is \(y_3 + \delta _3 \ge 1 + \textit{v}^{bv}_{i}\). The corresponding non-negativity constraint in \({{{\mathcal {Z}}}^{{\textit{bv}}}}\) is \(1 + \textit{v}^{bv}_{i} \ge 0\).

4.1.2 Operator variation

This type of variation is motivated by the assumption that a wrong comparison operator in a location invariant or transition guard may cause a property violation. We assume for the repair encoding that the operators \(\sim\) are indexed according to their order in the sequence \(\langle \; <, \le , =, \ge ,>\> \rangle\). The possible repairs are encoded by a fresh variation variable \(\textit{v}^{ov}_i\) where the value of \(\textit{v}^{ov}_i\) is the index of the corresponding comparison operator. For instance, the use of the < comparison operator as a repair is indicated by setting \(\textit{v}^{ov}_i= 1\).

We define operator variation constraints \({{{\mathcal {I}}}^{ov}}\) and \({{{\mathcal {G}}}^{{\textit{ov}}}}\) with the help of an n-ary exclusive or operation \(\bigoplus \limits _{i = 0 \ldots n}f_i\) which is satisfied iff exactly one of the formulas \(f_i\) is true:

Now, we construct an operator variation TDT constraint system \({{\mathcal {T}}}^{{\textit{ov}}} \equiv {{\mathcal {C}}}_0 \wedge {{\mathcal {A}}} \wedge {{\mathcal {R}}} \wedge {{\mathcal {D}}} \wedge {{\mathcal {I}}}^{{\textit{ov}}} \wedge {{\mathcal {G}}}^{{\textit{ov}}} \wedge {{\mathcal {U}}} \wedge {{\mathcal {L}}}\).

As an example for the operator variation encoding, consider the guard \(w>=1\) of transition \(\theta _2\) in Fig. 1b. The \({{{\mathcal {G}}}^{{\textit{ov}}}}\) contains the constraint \(w_2>=1 \wedge (\textit{v}^{{\textit{ov}}}_i= 0) \bigoplus ... \bigoplus w_2>1 \wedge (\textit{v}^{{\textit{ov}}}_i= 5)\).

4.1.3 Clock reference variation

This variation aims to repair property violations resulting from errors that can be traced back to the unintended use of a wrong clock variable. We uniquely identify every clock in the repair encoding by an index k. We introduce a fresh variation variable \(\textit{v}^{{\textit{cv}}}_i\) for every constraint with a clock c. Its assigned value k indicates that in the constraint, the clock \(c_k\) is to be used instead of c. For example, if \(y \le 2\) is a repaired constraint, where clock y has index \(k=1\), then \(\textit{v}^{{\textit{cv}}}_i= 1\).

We define the appropriate clock variation constraints \({\mathcal{I}^{{\textit{cv}}}}\) and \({{{\mathcal {G}}}^{{\textit{cv}}}}\):

From this we obtain the clock reference variation TDT constraint system \({{\mathcal {T}}}^{{\textit{cv}}} \equiv {{\mathcal {C}}}_0 \wedge {{\mathcal {A}}} \wedge {{\mathcal {R}}} \wedge {{\mathcal {D}}} \wedge {{\mathcal {I}}}^{{\textit{cv}}} \wedge {{\mathcal {G}}}^{{\textit{cv}}} \wedge {{\mathcal {U}}} \wedge {{\mathcal {L}}}\).

An example for the clock reference repair encoding is given by the guard \(y\ge 1\) of transition \(\theta _3\) in Fig. 1b. \({{{\mathcal {G}}}^{{\textit{cv}}}}\) contains the constraint \((y_3+\delta _3 \ge 1)\wedge (\textit{v}^{{\textit{cv}}}_i=0) \bigoplus ... \bigoplus (z_3+\delta _3 \ge 1)\wedge (\textit{v}^{{\textit{cv}}}_i=4)\).

4.1.4 Reset clock variation

This variation aims to repair a property violation by adding or removing clock resets. We introduce a variation variable \(\textit{v}^{{\textit{rv}}}_{c,\theta }\) for the transition \(\theta\) leaving location \(l_j\) and every clock c in the TDT. The reset status in the extended constraint system is inverted when \(\textit{v}^{{\textit{rv}}}_{c,\theta } \ne 0\): if c was not reset before, it will now be reset, and vice versa. This is encoded by the clock reset variation constraints \({{{\mathcal {R}}}^{{\textit{rv}}}}\) and \({{{\mathcal {D}}}^{{\textit{rv}}}}\):

As a result we obtain the reset clock variation TDT constraint system \({{\mathcal {T}}}^{{\textit{rv}}} \equiv {{\mathcal {C}}}_0 \wedge {{\mathcal {A}}} \wedge {{\mathcal {R}}}^{{\textit{rv}}} \wedge {{\mathcal {D}}}^{{\textit{rv}}} \wedge {{\mathcal {I}}} \wedge {{\mathcal {G}}} \wedge {{\mathcal {U}}} \wedge {{\mathcal {L}}}\).

To illustrate the clock reset repair encoding, consider the clock reset \(y:=0\) on transition \(\theta _2\) in Fig. 1b. \({{{\mathcal {R}}}^{{\textit{rv}}}}\) contains the constraint \(((y_3=0)\wedge (\textit{v}^{{\textit{rv}}}_{y,\theta _2}=0)) \vee ((y_3=y_2+\delta _2)\wedge (\textit{v}^{{\textit{rv}}}_{y,\theta _2}\ne 0))\).

4.1.5 Urgent location variation

Here we aim to repair cases where a faulty usage of urgent locations causes a property violation. Urgency of a location is modeled in the TDT constraint system by setting the location delay \(\delta _j\) to 0. We define a fresh variation variable \(\textit{v}^{{\textit{uv}}}_i\) for a location \(l_j\). For \(\textit{v}^{{\textit{uv}}}_i\ne 0\), the urgency for a location \(l_j\) is inverted. We encode this idea using the following urgency variation constraint \({{{\mathcal {U}}}^{{\textit{uv}}}}\):

We construct the urgent location variation TDT constraint system \({{\mathcal {T}}}^{{\textit{uv}}} \equiv {{\mathcal {C}}}_0 \wedge {{\mathcal {A}}} \wedge {{\mathcal {R}}} \wedge {{\mathcal {D}}} \wedge {{\mathcal {I}}} \wedge {{\mathcal {G}}} \wedge {{\mathcal {U}}}^{{\textit{uv}}} \wedge {{\mathcal {L}}}\).

As an example for the urgent location repair encoding, consider the location serReceiving reached by \(\theta _3\) in Fig. 1a. \({{{\mathcal {U}}}^{{\textit{uv}}}}\) contains the constraint \((\textit{v}^{{\textit{uv}}}_i\ne 0)\rightarrow (\delta _4=0)\).

4.2 Repair by variation analysis

The objective of the variation analysis is to provide hints to the system designer regarding which minimal syntactic changes to the considered model might prevent the violation of property \(\varPi\). Minimality here is considered with respect to the number of syntactic modifications that need to be performed in the considered TA model.

For the analysis, we first choose one of the variation TDTCS described before and denote it with \(\mathcal {T}^{*}\). We implement an analysis by using \(\mathcal {T}^{*}\) to derive an instance of the partial MaxSMT problem whose solutions yield candidate repairs for the timed automaton T. The partial MaxSMT problem takes as input a finite set of assertion formulas belonging to a fixed first-order theory. These assertions are partitioned into hard and soft assertions. The hard assertions \(\mathcal {F}_H^{*}\) are assumed to hold and the goal is to find a maximal subset \(\mathcal {F}' \subseteq \mathcal {F}^{*}_S\) of the soft assertions such that \(\mathcal {F}' \cup \mathcal {F}_H^{*}\) is satisfiable in the given theory.

For the purpose of our analysis, the hard assertions are formed by the conjunction

Note that the free variables of \(\mathcal {F}_H^{*}\) are exactly the variation variables \(\textit{v}^*_i\). Given a satisfying assignment \(\iota\) for \(\mathcal {F}_H^{*}\), let \(T_\iota\) be the timed automaton obtained from T by modifying a clock bound according to the variation value \(\iota (\textit{v}^*_i)\) and let Y\(_\iota\) be the TDT corresponding to Y in \(T_\iota\). Then \(\mathcal {F}_H^{*}\) guarantees that

1. 1.

   \(Y_\iota\) is feasible, and

2. 2.

   \(Y_\iota\) has no realization that witnesses a violation of \(\varPi\) in \(T_\iota\).

We refer to such an assignment \(\iota\) as a local clock repair for T and Y. To obtain a minimal local clock repair, we use the soft assertions given by the conjunction

Clearly, \(\mathcal {F}_H^{*} \wedge \mathcal {F}_S^{*}\) is unsatisfiable because \(\mathcal {T}^{*} \wedge \mathcal {F}_S^{*}\) is equisatisfiable with \({\mathcal {T}}\), and \({{\mathcal {T}}} \wedge \lnot \varPhi\) is satisfiable by assumption. However, if there exists at least one local clock repair for T and Y, then \(\mathcal {F}_H^{*}\) alone is satisfiable. In this case, the MaxSMT instance \(\mathcal {F}_H^{*} \cup \mathcal {F}_S^{*}\) has at least one solution. Every satisfying assignment of such a solution corresponds to a local repair that minimizes the number of syntactic modifications that need to be performed on T, and hence on the considered TA. Note that hard and soft assertions remain within a decidable logic. Using an SMT solver such as Z3, we enumerate all the optimal solutions for the partial MaxSMT instance and obtain a minimal local clock bound repair from each of them.

Example 2

We have applied the bound variation repair analysis to the TDT from Example 1. The following repairs exist:

1. 1.

   \(\textit{v}^{{\textit{bv}}}_{z,l_5} = -1\). This corresponds to a variation of the location invariant regarding clock z in location 5 of the TDT, corresponding to location client.serReceiving, to read \(z \le 1\) instead of \(z \le 2\). This indicates that the violation of the bound on the total duration of the transaction, as indicated by a return to the serReceiving location and a value greater than 4 for clock x, can be avoided by ensuring that the time taken for transmitting the ser message to the client is constrained to take exactly 1 time unit.

2. 2.

   A further computed repair is \(\textit{v}^{{\textit{bv}}}_{w,l_2} = -1\). Interpreting this variation in the context of Example 1 means that location db.reqReceived will be left when the clock w has value 1. In other words, the transmission of the message req to the db takes exactly one time unit, not between 1 and 2 time units as in the unrepaired model.

3. 3.

   Another computed repair is \(\textit{v}^{{\textit{bv}}}_{y,l_3}= -1\) and \(\textit{v}^{{\textit{bv}}}_{y,\theta _3}= -1\), which reduce the time delay in location db.reqProcessing by 1 time unit.

4. 4.

   No further minimal repair exists.

Examples of repairs according to the other analyses for the TDT in Fig. 1c include the following. The operator repair analysis returns, among others, a repair \(\textit{v}^{{\textit{ov}}}_{w,\theta _2}= 1\), which suggests to exchange the operator in the transition guard \(w\ge 1\) by < and to reduce the time for receiving the message req to be less than one time unit. The reference clock analysis returns a repair \(\textit{v}^{{\textit{cv}}}_{z,l_4}= y\). The repair exchanges the clock z in the clock constraint \(z\le 2\) by y, which implies that the model has to receive the message ser in less than one time unit since the guard \(y\ge 1\) is satisfied when entering location serReceiving. The reset clock analysis returns a repair \(\textit{v}^{{\textit{rv}}}_{x,\theta _2}= true\), which indicates to reset clock x during the transition leading into location reqProcessing. The urgent location analysis returns a repair \(\textit{v}^{{\textit{uv}}}_\textit{serReceiving} =true\) which suggests to turn serReceiving into an urgent location. This repair reduces the time for receiving message ser to zero.

4.2.1 Complexity considerations

The tool Z3 [46] computes a repair for partial MaxSMT instances without quantifiers. The repair analysis first executes quantifier elimination on \(\mathcal {F}_H^{*}\), which has a double exponential worst-case complexity in the number of quantifier variables [15]. The number of quantified variables in \(\mathcal {F}_H^{*}\) rises linearly with the length of the TDT. Afterwards, every repair analysis solves a MaxSMT problem for quantifier-free linear real arithmetic constraints. The complexity of the repair computation is determined by the number of time constraints in the TDT which increases with the length of the TDT. The complexity of quantifier-free linear real arithmetic is polynomial [30, 33]. The MaxSMT problem can be reduced in polynomial time to a MaxSAT problem, and a MaxSAT problem is an optimization problem in the complexity class NP [34]. We conclude that the quantifier elimination is the most complex computation in the analysis, which means that the overall complexity is in the worst case double exponential in the length of the TDT.

The synthesized repairs that lead to a TA \(T_\iota\) change the original TA T in fundamental ways, both syntactically and semantically. This brings up the question whether the synthesized repairs are admissible. In fact, one of the key questions is what notion of admissibility is meaningful in this context.

5.1 Admissibility criteria

From a syntactic point of view, the repair obtained from a satisfying assignment \(\iota\) of the MaxSMT instance ensures that \(T_\iota\) is a syntactically valid TA model, for instance, by placing non-negativity constraints on repaired clock bounds. In case repairs alter right hand sides of clock constraints to rational numbers, this can easily be transformed to integers by normalizing all clock constraints in the TA.

From a semantic perspective, the impact of the repairs is more profound. Since the repairs affect time bounds in location invariants and transition guards, as well as clock resets, the behavior of \(T_\iota\) may be fundamentally different from the behavior of T.

• The computed repair for one property \(\varPi\) may render another property \(\varPi '\) violated. To check admissibility of the synthesized repair with respect to the set of all properties \({\widehat{\varPi }}\) in the system specification, a full re-checking of \({\widehat{\varPi }}\) is necessary.

• A repair may have introduced zenoness and timelock [8] into \(T_\iota\). As discussed in [8], there exist both an over-approximating static test for zenoness as well as a model checking based precise test for timelocks that can be used to verify whether the repair is admissible in this regard.

• Due to changes in the possible assignment of time values to clocks, reachable locations in the TA T may become unreachable in \(T_\iota\), and vice versa. On the one hand, this means that some functionalities of the system may no longer be provided since part of the actions in T will no longer be executable in \(T_\iota\), and vice versa. Further, a reduction in the set of reachable locations in \(T_\iota\) compared to T may mean that certain locations with property violations in T are no longer reachable in \(T_\iota\), which implies that certain property violations are masked by a repair instead of being fixed. On the other hand, the repair leading to locations becoming reachable in \(T_\iota\) that were unreachable in T may have the effect that previously unobserved property violations become visible and that \(T_\iota\) possesses functionality that T does not have, which may or may not be desirable.

It should be pointed out that we assess admissibility of a repair leading to \(T_\iota\) with respect to a given TA model T, and not with respect to a correct TA model \(T^*\) satisfying \(\varPi\). Before we define an admissibility test based on functional equivalence, we introduce some necessary foundation.

5.2 Functional equivalence

While various variants of semantic admissibility may be considered, we are focusing on a notion of admissibility that ensures that a repair does not unduly change the functional behavior of the modeled system while adhering to the timing constraints of the repaired system. We refer to this as functional equivalence. The functional capabilities of a timed system manifest themselves in the sets of action or transition traces that the system can execute. For TAs T and \(T_\iota\) this means that we need to consider the languages over the action or transition alphabets that these TAs define. Considering the timed languages of T and \(T_\iota\), we can state that \({{\mathcal {L}}}_T(T) \ne {{\mathcal {L}}}_T(T_\iota )\) since the repair forces at least one timed trace to be purged from \({{\mathcal {L}}}_T(T)\). This means that equivalence of the timed languages cannot be an admissibility criterion ensuring functional equivalence.

At the other end of the spectrum we may relate the de-timed languages of T and \(T_\iota\). The de-time operator \(\alpha (T)\) is defined such that it omits all timing constraints and resets from any TA T. Requiring \({{\mathcal {L}}}(\alpha (T)) = {{\mathcal {L}}}(\alpha (T_\iota ))\) is tempting since it states that when eliminating all timing related features from T and from the repaired \(T_\iota\), the resulting action languages will be identical. However, this admissibility criterion would be flawed, since the repair in \(T_\iota\) may imply that unreachable locations in T will be reachable in \(T_\iota\), and vice versa. This may have an impact on the untimed languages, and even though \({{\mathcal {L}}}(\alpha (T)) = {{\mathcal {L}}}(\alpha (T_\iota ))\), it may be that \({{\mathcal {L}}}_{\mu }(T) \ne {{\mathcal {L}}}_{\mu }(T_\iota )\). To illustrate this point, consider the running example in Fig. 1a and assume the invariant in location client.serReceiving to be modified from \(z \le 2\) to \(z \le 1\) in the repaired TA \(T_\iota\). Applying the de-time operator to \(T_\iota\) implies that the location client.timeout, which is unreachable in \(T_\iota\), becomes reachable in the de-timed model. Since client.timeout is reachable in T, the TAs T and \(T_\iota\) are not functionally equivalent, even though their de-timed languages are identical. Notice that for the untimed languages it holds that \({{\mathcal {L}}}_{\mu }(T) \ne {{\mathcal {L}}}_{\mu }(T_\iota )\) since no timed trace in \({{\mathcal {L}}}_T(T_\iota )\) reaches location timeout, even though such a timed trace exists in \({{\mathcal {L}}}_T(T)\). In particular, \({{\mathcal {L}}}_{\mu }(T)\) contains the untimed trace \(\varTheta _0\varTheta _1\varTheta _2\varTheta _3\varTheta _4\), where \(\varTheta _4\) is the transition towards the location client.timeout, which is missing in \({{\mathcal {L}}}_{\mu }(T_\iota )\). As a consequence, we resort to considering the untimed languages of T and \(T_\iota\) when assessing functional equivalence and require \({{\mathcal {L}}}_{\mu }(T) = {{\mathcal {L}}}_{\mu }(T_\iota )\). It is easy to see that \({{\mathcal {L}}}_{\mu }(T) = {{\mathcal {L}}}_{\mu }(T_\iota ) \Rightarrow {{\mathcal {L}}}(\alpha (T)) = {{\mathcal {L}}}(\alpha (T_\iota ))\). In conclusion, the equivalence of the untimed languages ensures functional equivalence.

5.3 Admissibility test

Designing an algorithmic admissibility test for functional equivalence is challenging due to the computational complexity of determining the equivalence of the untimed languages \({{\mathcal {L}}}_{\mu }(T)\) and \({{\mathcal {L}}}_{\mu }(T_\iota )\). While language equivalence is decidable for languages defined by NBAs, it is undecidable for timed languages [4]. For untimed languages, however, this problem is again decidable [4]. The algorithmic implementation of the test for functional equivalence that we propose proceeds in two steps.

• First, the untimed languages \({{\mathcal {L}}}_\mu (T)\) and \({{\mathcal {L}}}_\mu (T_\iota )\) are constructed. This requires an untime transformation of T and \(T_\iota\) yielding NBAs representing \({{\mathcal {L}}}_\mu (T)\) and \({{\mathcal {L}}}_\mu (T_\iota )\). While the standard untime transformation for TAs [4] relies on a region construction, we propose a transformation that relies on a zone construction [23]. This will provide a more succinct representation of the resulting untimed languages and, hence, a more efficient equivalence test.

• Second, it needs to be determined whether \({{\mathcal {L}}}_\mu (T) = {{\mathcal {L}}}_\mu (T_\iota )\). As we shall see, the obtained NBAs are closed. Hence, we can reduce the equivalence problem for these \(\omega\)-regular languages to checking equivalence of the regular languages obtained by taking the finite prefixes of the traces in \({{\mathcal {L}}}_\mu (T)\) and \({{\mathcal {L}}}_\mu (T_\iota )\). This allows us to interpret the NBAs obtained in the first step as NFAs, for which the language equivalence check is a standard construction [24].

5.4 Automata for untimed languages

The construction of an automaton representing an untimed language, here referred to as an untime construction, has so far been proposed based on a region abstraction [4]. The region abstraction is known to be relatively inefficient since the number of regions is, among other things, exponential in the number of clocks [8]. We therefore propose an untime construction based on the construction of a zone automaton [23], which in the worst case is of the same complexity as the region automaton, but is more succinct in practice [12].

Definition 9

(Untimed Nondeterministic Büchi Automaton) Assume a TA T and the corresponding zone automaton \(\llbracket T\rrbracket _Z = (S_Z, s_Z^0, \varSigma _Z,\) \(\varTheta _Z)\). We define the untimed Nondeterministic Büchi automaton as the closed NBA \(B_T = (S, \varSigma ,\rightarrow , S_0,F)\) obtained from \(\llbracket T\rrbracket _Z\) such that \(S = S_Z\), \(\varSigma = \varSigma _Z \setminus \{\delta \}\), \(S_0 = \{s_Z^0\}\) and \(F=S\). For every transition in \(\varTheta _Z\) with a label \(a \in \varSigma\), we add a transition to \(\rightarrow\) created by the rule \(\frac{(l,z) \overset{\delta }{\leadsto } (l,z^\uparrow )\overset{a}{\leadsto }(l',z')}{ (l,z) \xrightarrow {a} (l',z')}\) with \(z^\uparrow = \{ v + \delta \in I(l) \mid v \in z, \delta \in {\mathbb {R}}_{\ge 0}\}\). In addition, we add self-transitions \((l,z) \xrightarrow {\tau } (l,z)\) to every state \((l,z) \in S_{B}\).

The following observations justify this definition:

• A timed trace of T may remain forever in the same location after a finite number of action transitions. In order to enable \(B_T\) to accept this trace, we add a self-transition labeled with \(\tau\) to \(\rightarrow\) for each state \(s \in S\) in \(B_T\), and later define s as accepting. These \(\tau\)-self-transitions extend every finite timed trace t leading to a state in \(S_\tau\) to an infinite trace \(t.\tau ^\omega\).

• The construction of the acceptance set F is more intricate. Convergent traces are often excluded from consideration in real-time model checking [8]. As a consequence, in the untime construction proposed in [4], only a subset of the states in S may be included in F. A repair may render a subgraph of the location graph of T that is only reachable by divergent traces, into a subgraph in \(T_\iota\) that is only reachable by convergent traces. However, excluding convergent traces is only meaningful when considering unbounded liveness properties, but not when analyzing timed safety properties, which in effect are safety properties. As argued in [12], unbounded liveness properties appear to be less important than timed safety properties in timed systems. This is due to the observation that divergent traces reflect unrealistic behavior in the limit, but finite prefixes of infinite divergent traces, which only need to be considered for timed safety properties, correspond to realistic behavior. This observation is also reflected in the way in which, e.g., UPPAAL treats reachability by convergent traces. In conclusion, this argument justifies our choice to define the zone automaton in the untime construction as a closed BA, i.e., \(F = S\).

We will now prove Theorem 2 and Theorem 3 to show that our admissibility test is correct. Theorem 2 states that the zone based untimed NBA construction actually preserves the untimed languages. In particular, we show that for a given TA T, \({{\mathcal {L}}}(B_T) = {{\mathcal {L}}}_\mu (T)\). For the proof, we use Untimed Bisimulation in order to replace the concrete time delay in T by the empty word \(\epsilon\), and to establish the desired language equality.

Definition 10

(Untimed Bisimulation (adapted from [12])) For a TTS \(H = (S, s_0,\varSigma , \rightarrow )\), let \(\rightarrow _\epsilon\) be the relation obtained from \(\rightarrow\) by replacing all delay transitions \((s_1, \delta , s_2)\) by \((s_1, \epsilon , s_2)\). Then, a TTS \(H = (S, s_0,\varSigma , \rightarrow )\) is said to untimed simulate another TTS \(H' = (S', s'_0, \varSigma , \rightarrow ')\) if there exists a relation \(R \subseteq S \times S'\) such that (1) \((s_0, s_0') \in R\) and (2) for all \((s_1, s'_1) \in R\), \(s_2 \in S\), and \(a \in \varSigma \cup \{\epsilon \}\) it holds that if \(s_1 \xrightarrow {a} s_2 \in \rightarrow _\epsilon\), then there exists \(s_2'\) with \(s'_1 \xrightarrow {a} s'_2 \in \rightarrow '_\epsilon\) and \((s_2,s'_2)\in R\). H and \(H'\) are untimed bisimilar if in addition \(H'\) untimed simulates H.

The proof of Theorem 2 is based on the insight from Lemma 1 that two untimed bisimilar TTSs have equivalent untimed languages.

Lemma 1

Given two TTS \(H_1\) and \(H_2\), if \(H_1\) untimed simulates \(H_2\), then \({{\mathcal {L}}}_\mu (H_1) \subseteq {{\mathcal {L}}}_\mu (H_2)\).

Proof

Assume that TTS \(H_1 = (S, s_0, \varSigma , \rightarrow )\) untimed simulates a TTS \(H_2 = (S', s'_0, \varSigma , \rightarrow ')\) with a simulation relation R. For any word v in \({{\mathcal {L}}}_\mu (H_1)\), we know that a timed trace \(\xi = (t_1, a_1)\ldots\) exists in \({{\mathcal {L}}}(H_1)\). We show that v is also in \({{\mathcal {L}}}_\mu (H_2)\) by inductively constructing a timed trace \(\xi '=(t'_1, a'_1)\ldots\) in \({{\mathcal {L}}}(H_2)\) with \(\mu (\xi )=\mu (\xi ')\). The induction iterates over the timed actions \((t_i, a_i)\) in \(\xi\).

Base Case: Initially, no timed action is taken in \(\xi\). The relation \((s_0, s'_0)\) is in R. For the induction step, we assume helper variables \(t_0=0\) and \(t'_0=0\).

Induction Step: For a timed action \((t_{i+1}, a_{i+1})\) in \(\xi\) and \((s_i, s'_i)\) in R, we now construct a timed action \((t'_{i+1}, a'_{i+1})\) in \(\xi '\).

For \((t_{i+1}, a_{i+1})\), a state \(s_*\) exists in \(H_1\) such that a delay transition \((s_i, t, s_*)\) with \(t = t_{i+1}-t_i\) and an action transition \((s_*, a_{i+1}, s_{i+1})\) are in \(\rightarrow\). The untimed bisimulation replaces delay transitions by \(\epsilon\), and defines \(\rightarrow _\epsilon\) and \(\rightarrow '_\epsilon\). Since \((s_{i}, s'_i)\) is in R and \((s_i, \epsilon , s_*)\in \rightarrow _\epsilon\), a state \(s'_*\) has to exist with \((s'_i, \epsilon ,s'_*)\in \rightarrow '_\epsilon\) and \((s_*, s'_*)\in R\). \((s'_i, \epsilon ,s'_*)\) exists only since a delay transition \((s'_i, t', s'_*)\) exists in \(\rightarrow '\). We construct \(t'_{i+1} = t'_i+t'\). Because \((s_*, a_{i+1}, s_{i+1})\) is in \(\rightarrow _\epsilon\) and \((s_*, s'_*)\in R\), a state \(s'_{i+1}\) in \(H_2\) has to exist such that \((s_{i+1}, s'_{i+1})\in R\) and \((s'_*, a_{i+1}, s'_{i+1})\in \rightarrow '_\epsilon\). We conclude \(a'_{i+1}=a_{i+1}\). Hence, we constructed the timed action \((t'_{i+1}, a'_{i+1})\) of \(\xi '\) and \((s_{i+1}, s'_{i+1})\in R\) holds.

In conclusion, we can construct for every timed word \(\xi\) in \({{\mathcal {L}}}(H_1)\), a timed word \(\xi '\) in \({{\mathcal {L}}}(H_2)\), such that \(\mu (\xi )=\mu (\xi ')\). \(\square\)

Additionally, the proof of Theorem 2 relies on the assumption that the timed language of the zone automaton \(\llbracket T \rrbracket _Z\) is identical to the timed language of T, which we state in the following lemma.

Lemma 2

(Zone Language Equivalence) Let \(\llbracket T \rrbracket _Z\) be a zone automaton derived from a TA T, then \({{\mathcal {L}}}_T(\llbracket T \rrbracket _Z) = \mathcal{L}_T(T)\).

Proof

The proof of this lemma can be derived from the proofs of Theorem 1 and Theorem 2 given in the full version of [45], which together prove that the reachable states in the transition system of T are also reachable in \(\llbracket T \rrbracket _Z\), and vice versa. The proofs rely on an induction over the length of the traces of T and \(\llbracket T \rrbracket _Z\) and imply an equivalence of the sets of traces of T and \(\llbracket T \rrbracket _Z\). This implies \({{\mathcal {L}}}_T(\llbracket T \rrbracket _Z) = {{\mathcal {L}}}_T(T)\). \(\square\)

Theorem 2

(Correctness of Untimed NBA Construction) For an untimed NBA \(B_T\) derived from a TA T according to Definition 9 it holds that \({{\mathcal {L}}}(B_T) = \mathcal{L}_\mu (T)\).

Proof

Assume a zone automaton \(\llbracket T \rrbracket _Z = (S_Z, s_Z^0, \varSigma _Z , \varTheta _Z)\) for a TA T and let \(B_T = (S_B, \varSigma _B,\rightarrow , S^0_B,\) F) be the associated untimed NBA obtained according to Definition 9 with \(\llbracket T \rrbracket _Z\).

Lemma 2 permits us to prove Theorem 2 by showing \({{\mathcal {L}}}({B_T}) = {{\mathcal {L}}}_\mu (\llbracket T \rrbracket _Z)\). We prove the conjecture by proving the stricter condition that the zone automaton \(\llbracket T \rrbracket _Z\) and the untimed NBA \(B_T\) are untimed bisimilar. We may then conclude language equivalence by Lemma 1 and bisimilarity. It is appropriate to compare an untimed NBA \(B_T\) to a zone automaton \(\llbracket T \rrbracket _Z\) by untimed bisimulation since \(B_T\) is an untimed automaton, in particular, an untimed zone automaton.

We now show that \(R = \{((l, z_Z), (l, z_{B}))| z_Z^\uparrow = z_B^\uparrow \wedge (l, z_Z) \in S_Z \wedge (l, z_{B}) \in S_{B}\}\) is an untimed bisimulation relation. R is an untimed bisimulation relation for the alphabet \(\varSigma = (\varSigma _B \setminus \{\tau \}) \cup (\varSigma _Z \setminus \{\delta \})\), where the delay transitions \(\delta\) and \(\tau\) are removed by the construction of the untimed bisimulation.

We show for an arbitrary \(((l, z_Z), (l, z_{B})) \in R\) that \(((l', z'_Z), (l', z'_Z)) \in R\) for all actions \(a \in \varSigma\). \(z_{B} \subseteq z_Z\) holds by construction of \(B_T\) since transitions in \(B_T\) reach a state after taking an action transition. Hence, there are two cases to be considered in order to determine whether \(z_Z^\uparrow = z_{B}^\uparrow\):

1. 1.

   If \(z_Z = z_{B}\), then the untime construction creates a transition \((l, z_{B}) \overset{a}{\leadsto } (l', z'_Z)\in \rightarrow\) iff \((l, z_Z)\xrightarrow {\delta }(l, z_Z^\uparrow )\xrightarrow {a}(l', z'_Z) \in \varTheta _Z\) exists.

2. 2.

   If \(z_Z = z_{B}^\uparrow\), then the untime construction creates a transition \((l, z_{B}) \overset{a}{\leadsto } (l', z'_Z)\in \rightarrow\) iff \((l, z_Z)\xrightarrow {a}(l', z'_Z) \in \varTheta _Z\) exists.

In both cases it holds that \(((l', z'_Z), (l', z'_Z)) \in R\). Thus, R is a bisimulation relation. The tuple \(((l_0, z_0), (l_0, z_0))\) of the initial states of \(\llbracket T \rrbracket _Z\) and \({B_T}\) is in R, since \(S_B^0 = \{s_Z^0\}\) holds by the definition of the untime construction, and trivially \(z_0^\uparrow = z_0^\uparrow\). This implies that \(B_T\) and \(\llbracket T \rrbracket _Z\) are untimed bisimilar and \({{\mathcal {L}}}({B_T}) = {{\mathcal {L}}}_\mu (\llbracket T \rrbracket _Z)\) holds. \(\square\)

5.5 Equivalence check for untimed languages

Given that the zone automaton construction delivers closed NBAs we can reduce the admissibility test \({{\mathcal {L}}}_{\mu }(T) = {{\mathcal {L}}}_{\mu }(T_\iota )\) defined over infinite languages to an equivalence test over the finite prefixes of these languages, represented by interpreting the zone automata as NFAs. The following theorem justifies this reduction.

Theorem 3

(Language Equivalence of Closed NBAs) Given closed NBAs B and \(B'\), if \({{\mathcal {L}}}_{\text {f}}(B) = {{\mathcal {L}}}_{\text {f}}(B')\) then \({{\mathcal {L}}}(B) = {{\mathcal {L}}}(B')\).

Proof

For a closed NBA B, it is easy to see that \({{\mathcal {L}}}_{\text {f}}(B) = \text {pref}({{\mathcal {L}}}(B))\). Assume \({{\mathcal {L}}}_{\text {f}}(B) = {{\mathcal {L}}}_{\text {f}}(B')\) and \({{\mathcal {L}}}(B) \ne {{\mathcal {L}}}(B')\). This means that, w.l.o.g., \((\exists v)(v \in {{\mathcal {L}}}(B) \wedge v \notin {{\mathcal {L}}}(B'))\). This implies that there is no accepting run on some v in \(B'\). Since \(B'\) is closed, the only way of not accepting v is that \(B'\) blocks when reading a finite prefix \({\hat{v}} = v_1, \ldots , v_n\) of v. Hence, \({\hat{v}} \in {{\mathcal {L}}}_{\text {f}}(B) \wedge {\hat{v}} \notin {{\mathcal {L}}}_{\text {f}}(B')\), which contradicts \({{\mathcal {L}}}_{\text {f}}(B) = {{\mathcal {L}}}_{\text {f}}(B')\). Therefore, \({{\mathcal {L}}}(B) = {{\mathcal {L}}}(B')\). \(\square\)

5.6 Complexity of the admissibility test

In order to test admissibility, we generate the state space of the original TA and the TA to which we apply the repair. The computation of the state space uses real-time model checking which is in PSPACE [3]. Afterwards, we interpret the two state spaces as NFAs and perform a language equivalence test. Checking language equivalence of two NFAs is decidable in NP [21]. The overall complexity of the admissibility test is thus in PSPACE.

5.7 Discussion

One may want to adapt the admissibility test so that it only considers divergent traces, e.g., in cases where only unbounded liveness properties need to be preserved by a repair. This can be accomplished as follows. First, an overapproximating non-zenoness test [8] can be applied to T and \(T_\iota\). If it shows non-zenoness, then one knows that the respective TA does not include convergent traces. If this test fails, a more expensive test needs to be developed. It requires a construction of the untimed NBA using the approach from [4], and subsequently a language equivalence test of the untimed languages accepted by the untimed NBAs using, for instance, the automata-theoretic constructions proposed in [13]. Checking language equivalence of two NBAs is in the complexity of PSPACE [14]. Creating the untimed NBA, which is the input to the equivalence check, is also in PSPACE. So the overall complexity of this analysis remains in PSPACE.

We implemented the repair computations and the admissibility test in the tool TarTar. The software architecture of TarTar is depicted in Fig. 3b. The orange rectangles in the figure represent external tools that TarTar calls in the course of the repair analysis. Uppaal is a state-of-the-art and closed-source model checking tool, which TarTar uses to compute a TDT for a given model and property. The SMT solver Z3 [18] is used to solve the generated partial MaxSMT problems. In order to check the admissibility of a repair, TarTar uses opaal and the AutomataLib component of LearnLib [25] since they conveniently provide functionality used in the implementation of the admissibility test.

TarTar Tool

Full size image

6.1 Data flow architecture

TarTar consists of many computation steps. For example, a TDT is parsed internally and stored as a Trace. This Trace is then modified and exported as SMT-LIB2 [7] code. We define a computation step of TarTar as the computation transforming input into result artifacts. This focus on artifacts ensures a highly cohesive architecture and clear interfaces between any two computation steps. Computation steps with identical objectives are grouped into a project. This results in four projects depicted by blue rectangles in Fig. 3b.

• HMI denotes the user interfaces of TarTar. The user inputs a timed model. TarTar then calls the project Repair Computation using a faulty timed model as a parameter. In case that the model is correct, TarTar calls the project Modification Seeding.

• Modification Seeding seeds modifications into a correct model and then repairs the resulting faulty models by computing repairs using Repair Computation. We use this analysis in Sect. 7 in order to benchmark the Repair Computation analyses.

• Repair Computation computes candidate repairs for a faulty timed model, applies these repairs to the model and finally automatically calls the Admissibility Test.

• Admissibility Test checks for every repaired model whether the computed repair is admissible.

6.2 Control flow architecture

TarTar computes iteratively a set of repairs for a given faulty Uppaal model and a given property \(\varPi\) using the following steps:

1. 0.

   Counterexample Creation. TarTar calls Uppaal to verify the model against \(\varPi\). In case \(\varPi\) is violated, it stores a shortest symbolic TDT witnessing the violation in XML format.

2. 1.

   Diagnostic Trace Creation. TarTar parses the model and the TDT into a data structure Trace. To add potential repairs, TarTar copies the trace and replaces the constraints that will potentially be subject to a repair by their modified variants. The modified trace is then translated to a logic constraint system \({\mathcal {T}}^*\), represented in SMT-LIB2 code.

3. 2.

   Repair Computation. Z3 [18] then solves a MaxSMT problem on the modified trace constraint system, computing a repair in which the number of unmodified constraints on the variation variables of the form \(\textit{v}^*=0\) is maximized. Since Z3 can solve a MaxSMT problem only for quantifier-free linear real arithmetic, TarTar first runs a quantifier elimination on the constraint system \(\forall \delta _j, c_j.\, {{\mathcal {T}}}^{*} \Rightarrow \varPhi\) of \(\mathcal {F}_H^{*}\).

4. 3.

   It then solves the MaxSMT problem with soft constraints requiring \(\textit{v}^*=0\) for all variation variables. In case no solution is found, TarTar terminates. Otherwise, TarTar applies the repair to the faulty model and returns a repaired model.

5. 4.

   Admissibility Test. TarTar checks the admissibility of a repair and compares the untimed languages of the faulty and repaired models. TarTar calls the model checker opaal in order to compute the timed transition systems (TTS) of the original and the repaired Uppaal model. We modified the opaal model checker in such a way that it returns the TTS for a model. TarTar then checks whether the two TTS have equivalent untimed languages, in which case the repair is admissible. This check is implemented using the library AutomataLib. In case the two TTS are not equivalent, the admissibility test returns a trace as a witness for the difference.

6. 5.

   Iteration. TarTar enumerates all repairs, i.e., every combination of the same kind of constraint modifications that corrects the TDT. The repairs are iteratively enumerated starting with the ones that require the smallest number of modifications to the model. After a repair is computed, the combination of modified variables that has been found is prevented from being reconsidered for future repairs by setting these modification variables to 0 using hard asserts. TarTar then proceeds with attempting to compute further, previously unconsidered repairs.

6.3 Component architecture

TarTar component architecture

Full size image

We implemented TarTar with the general infrastructure depicted in Fig. 4. The interface Job provides a general abstraction for an algorithm and specifies the necessary input and result values of the algorithm by the class Description. TarTar contains a Job for the projects Modification Seeding, Repair Computations and Admissibility Test. The class Session executes a Job and derivations of Session provide the different interfaces to the user. With this infrastructure, the analysis implementation in TarTar is independent from the implementation of the user interfaces, thus reducing coupling and improving modifiability of the code.

6.4 Implementation details

We implemented the different projects that constitute TarTar in Java and use the build-management tool maven [37] to manage the dependencies between the projects. TarTar interacts differently with the external tools that are needed for different purposes. It calls Uppaal via the command-line interface in order to generate a TDT, calls Z3 via its API to compute a repair. For the admissibility test, it calls opaal using a command-line script and the AutomataLib as an included Java library. For the implementation of the TarTar analyses the following two details are essential.

• We modify constraints in an Uppaal model in order to apply a repair or to seed a fault. Since neither clock constraints nor transitions possess explicit unique identifiers in an Uppaal model, it is not obvious which constraint to change. We therefore uniquely identify a constraint by traversing the constraints in the sequence stored in the Uppaal model file and use the constraint index in this sequence as its identifier.

• The complexity of the algorithms for solving quantifier elimination and the MaxSMT problem rise with the number of variables in the SMT model. We therefore reduce the number of variables by exploiting implied equality constraints. For example, a variable \(c_j\) is created for every clock c in every step j of the TDT. We eliminate \(c_j\) explicitly before quantifier elimination by replacing it with the term \(\sum \nolimits _{i \in r\ldots j}d_i\), where \(d_i\) is the time delay at step i in the trace and r is the last step before j where c was reset.

We evaluate the repair analyses by applying TarTar to the database model in Example 1 and to more complex case studies of different sizes.

7.1 Database model repairs

We applied TarTar to the database model in Fig. 1. TarTar finds two admissible clock bound repairs. A replacement of \(w\le 2\) by \(w\le 1\) and a replacement of \(y\le 1\) by \(y\le 0\) and \(y\ge 1\) by \(y\ge 0\) repairs the database model. With operator variation repair analysis, TarTar finds two admissible repairs that replace the operator in the clock constraint \(w>=1\) by < or \(<=\), respectively. With clock reference repair analysis, TarTar finds 13 admissible clock reference modification repairs, each involving two modifications. Nine repairs replace y in the constraints \(y \le 1\) and \(y \ge 1\) by a selection from the set of clocks z, x and w. Four repairs replace y in the constraint \(y \le 1\) by w or x, and w in the constraint \(w\ge 1\) by y or z. Applying the reset repair analysis, TarTar finds four admissible repairs. One repair removes the reset of clock y, another removes the reset of clock z, and two repairs add a reset of clock x either on the transitions towards the location reqProcessing or the transition towards the location serReceiving. Applying the urgency location repair analysis, TarTar finds only two inadmissible and no admissible repairs, one setting the location reqAwaiting and the other the location serReceiving to urgent.

The computed repairs are reasonable and we expected them. We remain to evaluate whether TarTar can analyze more complex models.

7.2 Evaluation strategy

In order to perform an experimental evaluation of the repair analyses both qualitatively and quantitatively, we need a set of timed automata models that violate given properties. Such models are not publicly available in significant numbers and to the best of our knowledge, no benchmark suite for property violating timed automata models exists. As a consequence, the evaluation of our analyses is based on ideas taken from mutation testing [26]. Mutation testing evaluates a test set by systematically modifying the program code to be tested and computing the ratio of modifications that are detected by the test set. In adopting this strategy, we seed modifications in existing models and check whether those can be successfully repaired by our automated repair analyses. Thereby, we evaluate the quality of our repair technique.

7.2.1 Modification seeding

modifies a given TA model syntactically in one of the following ways:

• Replacing the comparison operator in a clock constraint by \(\{<, \le , =, \ge , >\}\),

• Swapping a clock name referenced in a clock constraint or invariant with some other clock name occurring in the original model,

• Modifying the set of clocks that are reset in any given transition,

• switching for any location whether it is urgent or not,

• Or modifying the bound of a single clock constraint by an amount selected from the set \(\{-10, -1, +1, +0.1M, +M\}\), where M is the maximal clock bound occurring in a given model. Our observation was that making either a small modification that is close to the bound value or a modification in the order of the maximal bound value M often introduces a property violation in the considered models.

The result is a modified TA that contains a single modification. TarTar automatically checks for every modified TA whether it violates a given property, in which case a TDT is generated.

7.2.2 Experimental procedure

TarTar applies modification seeding to several models used for experimentation and generates a set of TDTs by performing model checking for a given property on each of the modified models. For every computed TDT, TarTar performs the above defined repair analyses one after another, and measures the ratio of TDTs for which the analyses compute at least one repair.

7.3 Experiments

We have applied this evaluation strategy to eight UPPAAL models (see Table 1). Not all of the models that we considered have been published with a property that can be violated by mutating a clock constraint. For those models, we manually identify a suitable timed safety property specifying an invariant condition which can then be violated by some of the proposed mutations. In particular, we add a property to the Bando [43] model which ensures that, for as long as the sender is active, its clock never exceeds the value of 28, 116 time units. In the FDDI token ring protocol [43], the property that we use checks whether the first member of the ring never remains in any given state for more than 140 time units. The Viking model is taken from the set of test models of opaal [39]. For this model we use a property that checks whether one of the Viking processes can only enter a safe state during the first 60 time units. Note that all of these properties are satisfied by the original models prior to modification seeding.

We applied modification seeding to the models given in Table 1 and analyzed the obtained TDTs using the above described repair analyses implemented in TarTar. All analyses were performed on a computer with an i7-6700K CPU (4.00GHz), 60GB of RAM and a 64 bit Linux operating system. We summarize the results of this experiment per considered model (Table 1) and per type of considered repair (Table 2). In Table 3, we give insight into a subset of the repair analysis results for the cases where the repair analysis was of the same type as the seeded modification.

In Table 1, we give in the first three rows the source of the model as well as its number of locations and transitions. In every model, we modify the time constraints as described above, which results in a number #Seed of modifications and the same number of modified models. Uppaal analyzes each modified model and finds #TDT property-violating models. \(\textit{Time}_{\textit{UP}}\) is the maximal time that Uppaal needs to create a TDT for the property violating models, and the longest TDT has a length of Length. Overall, TarTar computed a number #Repair of repairs for the TDTS, of which #Admissible are admissible. We say a TDT is solved when at least one admissible repair is computed by a repair analysis. #Solved states the number of solved TDTs. The computation effort for a repair analysis is given by the time \(\textit{Time}_{\textit{QE}}\) for successful quantifier elimination, the number of timeouts #Timeout that occurred during quantifier elimination after 10 minutes, the average time \(\textit{Time}_{\textit{Repair}}\) to compute a repair, and the memory consumption \(\textit{Mem}_\textit{Repair}\) for the overall analysis. The constraint system that Z3 solves has the count #Variable of variables and #Constraint of constraints. The effort for the admissibility test is given in time \(\textit{Time}_{\textit{Adm}}\) and memory \(\textit{Mem}_\textit{Adm}\). All times are given in seconds and memory consumption in MB. Notice that we omit the lines pertaining to the modification seeding and TDT computation in Table 2 since they are irrelevant there.

We illustrate the evaluation procedure using an instance of the pacemaker case study, which is a real world model of realistic size. One of the seeded bound modifications increases a location invariant of this model which controls the minimal heart period to remain within a range from 400 to 1, 600 time units. The modification allows the pacemaker to delay an induced ventricular beat for too long so that this violates the property that the time between two ventricular beats of a heart is never longer than the maximal heart period of 1, 000. TarTar finds three repairs. The first repair reduces the maximal time delay between two articular heartbeats such that the pacemaker cannot and no longer needs to trigger the articular heartbeat. The second repair reduces the maximal time delay between two ventricular heartbeats such that the pacemaker cannot trigger the first ventricular heartbeat. Both repairs changes the heart behavior and removes functional behavior of the pacemaker and, hence, are classified as inadmissible. In the model context, this appears to be reasonable since the repairs restrict the environment of the pacemaker, and not the pacemaker itself. The third repair is admissible and reduces the bound modified during the seeding of bound modifications by 1199.5. The minimal heart period is then also below or equal to the maximal heart period of 1000.

Overall, TarTar seeded 4508 modifications. This resulted in 175 TDTs in total. 60 TDTs were due to bound modification, 72 were due to operator variation, 27 were due to changing the clock reference, 8 were due to complementing the reset of clocks and 8 were due to the switching of urgent locations (see Table 3). TarTar found in total 5355 repairs, out of which 1,169 were admissible. It found at least one admissible repair for 122 (69%) of the 175 TDTs. The maximal number of modified constraints in an admissible repair computed for a single TDT using all types of repair analysis was 25. A total of 4222 repairs were of the same type as the seeded modification. Out of these same type repairs, 682 were admissible. At least one admissible same type repair exists for 102 (58%) of the 175 TDTs.

7.4 Result interpretation

7.4.1 Pacemaker instance results

Our repair strategy minimizes the number of repairs but does not optimize the computed value. For instance, in the pacemaker model the computed repair of 1199.5 time units would be a correct and admissible repair even if the value was reduced by 600 time units, which would be the minimal possible repair value.

7.4.2 Modification seeding results

Few of the seeded modifications resulted in a property violation. TarTar seeded 4,508 faults, which led to 175 TDTs, thus only 3.9% of these modifications result in a TDT. This supports the hypothesis that, in practice, often times only few time constraints impact the satisfaction of a checked property.

7.4.3 Repair results where the seeded modification is of arbitrary type

TarTar computes at least one admissible repair by bound modification for 85 (48%), by operator variation for 51 (29%), by clock reference for 35 (20%), by clock reset for 13 (7%) and by urgent location for 37 (21%) of the 175 TDTs. Every analysis on its own computes less admissible repairs than the combination of all repair analyses, which solves 122 (69%) of the 175 TDTs. The largest number of constraints that an admissible repair modified was 25, which is less than anticipated. This low number of modified constraints allow us to infer that only few constraints have an impact on whether a property is violated or not.

TarTar does not find an admissible repair for every TDT. For instance, TarTar finds an admissible repair for 53 TDT of the 60 TDTs created by bound modification, but only 3 analyses result in a timeout (Table 3). Hence, there exist 4 TDTs for which no admissible repair was computed even though they did not result in a timeout. There are two reasons for this phenomenon. Notice that a TDT is caused by modification seeding in which a constraint c in a model is modified. First, the seeding of a modification in the model may enable or disable transitions and, as a consequence, change the functional behavior of the unmodified model. A repair computed by TarTar may not precisely undo the modification, and therefore it cannot be guaranteed that the repaired model is functionally consistent with the unmodified model. Second, even if the modified model is functionally consistent with the unmodified model, the computed repair may not undo the modification and at the same time be inadmissible.

7.4.4 Computational effort

A comparison of \(T_{\textit{QE}}\) and \(T_R\) in every table confirms that the computational effort for the repair computation is largely determined by the quantifier elimination step, as we also concluded from the complexity analysis for the repair analysis. Only the urgent location repair consumes more computation time during the repair computation than during the quantifier elimination step. We expect that in light of the observed 226 timeouts, a more efficient quantifier elimination procedure would lead to a significantly higher number of repairs that could be computed without encountering a timeout. Furthermore, the number of timeouts, and thus the computation time needed for the repair, seems to correlate with the length of the analyzed TDT. With 86 the SBR model includes the largest number of timeouts and the third longest TDT with a length of 84 steps. The bando model has the third most timeouts (46) and the longest TDT. Obviously, the longer the TDT, the larger the resulting constraint system, leading to increased computational effort. With 1, 156 variables and 8, 144 constraints, the bando model yields the largest constraint system. The SBR model has the second largest constraint system with 765 variables and 1, 211 constraints. The model FDDI has a shorter TDT with a length of 11 transitions and a much smaller constraint system with 116 variables and 272 constraints. In order to provide some statistical evidence for the impact of the TDT length and the intrinsic model complexity on the computational effort we analyzed the statistical relationship between the length of the TDT and the computation time for a repair (\(T_r\) = \(\textit{T}_{\textit{QE}}\) + \(\textit{T}_{\textit{R}}\)) as well as the relationship between #Variable and \(T_r\), both by estimating Kendall’s tau [20] for every TDT. Kendall’s tau is a measure for the ordinal association between two measured quantities. A correlation computed by Kendall’s tau estimation approach is considered significant if the probability p that there is actually no correlation in a larger data set is below a certain threshold. We use the commonly applied significance threshold of 0.05. The length of a TDT is significantly related (\(\tau _1=0.521\), \(p<.001\)) to \(T_r\). Also #Variable is significantly related (\(\tau _2=0.496\), \(p<.001\)) to \(T_r\). From this we conclude that the complexity of a repair depends not only on the TDT length, but also on the intrinsic complexity of the model as expressed by the number of variables occurring in the model.

We also observe that the admissibility test requires more computational resources than the repair computation. The maximum amount of memory used for the admissibility test was \(1,251\text {MB}\) in contrast to \(37.16\text {MB}\) for the repair computation. This is in line with our expectation since the admissibility test involves searches of the state space of the full NTA, while the repair analyses only consider a single TDT.

Modifying states from urgent to non-urgent during modification seeding resulted in only 8 TDTs. This low number is due to the observation that the considered models contain only very few urgent states. Modifying non-urgent states to urgent ones, however, did not lead to a single property violation resulting in a TDT. The rationale is that urgency ensures to leave a state immediately without a delay which leads to a restriction rather than a relaxation regarding the time budget spent along an execution trace. As a consequence, making a state urgent does not cause a property violation in many models since the type of the checked properties is typically time bounded reachability, and a restricted time budget does not make it more likely that the property is violated.

7.4.5 Results of repairs that have the same type as the seeded modification

Recall that we seed different types of modifications that correspond to the different types of repair analyses that we propose. For every type of a repair analysis, we now compare the probability to compute an admissible repair when the seeded modificaton is of the same type as the repair (see Table 3) with the case when the seeded modification is of arbitrary type (see Table 2). Bound modification analysis repairs with a higher probability (88% to \(48\%\)) a TDT with a seeded bound modification than a modification of an arbitrary type. Also, operator modification analysis (\(52\%\) to \(29\%\)), clock reference analysis (\(33\%\) to \(20\%\)) and clock reset analysis (\(12\%\) to \(7\%\)) compute a repair with a higher probability for the same type of seeded fault as a modification of an arbitrary type. Only the urgent location analysis computes a repair with a lower probability (\(12\%\) to \(21\%\)) for a TDT with a seeded urgent location modification than for a modification of arbitrary type. In summary, with the exception of the urgent repair analysis, an admissible repair is computed with a higher probability if the repair analysis is of the same type as the seeded modification.

We finally observe that the repair computations of a seeded modification of an arbitrary type (Table 2) and repair computations of the same type as the seeded modification (Table 3) require similar computational effort in terms of time and memory consumption. We conclude that the computational effort of a repair analysis is independent of the type of a seeded modification that it repairs.

We have presented an approach to derive minimal repairs for timed reachability properties of NTA models from TDTs returned as counterexamples during model checking. The objective of this repair synthesis is to facilitate fault localization and debugging of such models during the design process. Our approach includes a formalization of TDTs using linear real arithmetic, a repair strategy based on MaxSMT solving, the definition of an admissibility criterion and test for the computed repairs, the development of an analysis and repair tool, and the application of the proposed method to a number of case studies of realistic complexity. To the best of our knowledge, this is the first rigorous treatment of counterexamples in real-time model checking. We have nonetheless observed that our analysis computes a significant number of admissible repairs within realistic computation time bounds and memory consumption.

In future work we plan to explore the interplay between different repairs that are computed for a repaired system that still violates a property, and develop refined strategies to select promising repairs from a repair set. A further generalization of the analysis is to not only compute clock constraint modifications for faulty models but also to compute possible relaxations of clock constraints for correct models in order to support design space exploration.