Refinement of Trace Abstraction for Real-Time Programs

Abstract

Real-time programs are made of instructions that can perform assignments to discrete and real-valued variables. They are general enough to capture interesting classes of timed systems such as timed automata, stopwatch automata, time(d) Petri nets and hybrid automata. We propose a semi-algorithm using refinement of trace abstractions to solve both the reachability verification problem and the parameter synthesis problem for real-time programs. We report on the implementation of our algorithm and we show that our new method provides solutions to problems which are unsolvable by the current state-of-the-art tools.

1 Introduction

Model-checking is a widely used formal method to assist in verifying software systems. A wide range of model-checking techniques and tools are available and there are numerous successful applications in the safety-critical industry and the hardware industry – in addition the approach is seeing an increasing adoption in the general software engineering community. The main limitation of this formal verification technique is the so-called state explosion problem. Abstraction refinement techniques were introduced to overcome this problem. The most well-known technique is probably the Counter Example Guided Abstraction Refinement (CEGAR) method pioneered by Clarke et al. [12]. In this method the state space is abstracted with predicates on the concrete values of the program variables. The (counter-example guided) refinement of trace abstraction (TAR) method was proposed recently by Heizmann et al. [17, 18] and is based on abstracting the set of traces of a program rather than the set of states. These two techniques have been widely used in the context of software verification. Their effectiveness and versatility in verifying qualitative (or functional) properties of C programs is reflected in the most recent Software Verification competition results [6, 11].

Analysis of Timed Systems. Reasoning about quantitative properties of programs requires extended modeling features like real-time clocks. Timed Automata [1] (TA), introduced by Alur and Dill in 1989, is a very popular formalism to model real-time systems with dense-time clocks. Efficient symbolic model-checking techniques for TA are implemented in the real-time model-checker Uppaal [4]. Extending TA, e.g., with the ability to stop and resume clocks (stopwatches), leads to undecidability of the reachability problem [9, 20]. Semi-algorithms have been designed to verify hybrid systems (extended classes of TA) and are implemented in a number of dedicated tools [15, 16, 19]. However, a common difficulty with the analysis of quantitative properties of timed automata and extensions thereof is that ad-hoc data-structures are needed for each extension and each type of problem. As a consequence, the analysis tools have special-purpose efficient algorithms and data-structures suited and optimized only towards their specific problem and extension.

In this work we aim to provide a uniform solution to the analysis of timed systems by designing a generic semi-algorithm to analyze real-time programs which semantically captures a wide range of specification formalisms, including hybrid automata. We demonstrate that our new method provides solutions to problems which are unsolvable by the current state-of-the-art tools. We also show that our technique can be extended to solve specific problems like robustness and parameter synthesis.

Related Work. The refinement of trace abstractions (TAR) was proposed by Heizmann et al. [17, 18]. It has not been extended to the verification of real-time systems. Wang et al. [23] proposed the use of TAR for the analysis of timed automata. However, their approach is based on the computation of the standard zones which comes with usual limitations: it is not applicable to extensions of TA (e.g., stopwatch automata) and can only discover predicates that are zones. Their approach has not been implemented and it is not clear whether it can outperform state-of-the-art techniques e.g., as implemented in Uppaal. Dierks et al. [14] proposed a CEGAR based method for Timed Systems. To the best of our knowledge, this method got limited attention in the community.

Tools such as Uppaal [4], SpaceEx [16], HyTech [19], PHAver [15], verifix [21], symrob [22] and Imitator [2] all rely on special-purpose polyhedra libraries to realize their computation.

Our technique is radically different to previous approaches and leverages the power of SMT-solvers to discover non-trivial invariants for the class of hybrid automata. All the previous analysis techniques compute, reduce and check the state-space either up-front or on-the-fly, leading to the construction of significant parts of the statespace. In contrast our approach is an abstraction refinement method and the refinements are built by discovering non-trivial program invariants that are not always expressible using zones, or polyehdra. This enables us to successfully analyze (terminate) instances of non-decidable classes like stopwatch automata. A simple example is discussed in Sect. 2.

Our Contribution. In this paper, we propose a refinement of trace abstractions (TAR) technique to solve the reachability problem and the parameter synthesis problem for real-time programs.

Our approach combines an automata-theoretic framework and state-of-the-art Satisfiability Modulo Theory (SMT) techniques for discovering program invariants. We demonstrate on a number of case-studies that this new approach can compute answers to problems unsolvable by special-purpose tools and algorithms in their respective domain.

Fig. 1.

Finite automaton $A_1$

2 Motivating Example

The finite automaton $A_1$ (Fig. 1), accepts the regular language $\mathcal{L}(A_1) = i.t_0.t_1^*.t_2$. By interpreting the labels of $A_1$ according to the Table in Fig. 1, we can view it as a stopwatch automaton with 2 clocks, x and z, and one stopwatch y (the variables). Each label defines a guard g (a Boolean constraint on the variables), anupdate u which is a (discrete) assignment to the variables, and a rate (vector) r that defines the derivatives of the variables.¹ We associate with a sequence $w=a_0.a_1.\cdots .a_n \in \mathcal {L}(A_1)$, a (possibly empty) set of timed words, $\tau (w)$, of the form $(a_0,\delta _0).\cdots$ $(a_n,\delta _n)$ where $\delta _i \ge 0, i\in [0\ldots n]$. For instance, the timed words associated with $i.t_0.t_2$ are of the form $(i,\delta _0).(t_0,\delta _1).(t_2,\delta _2)$, for all $\delta _i \in \mathbb {R}_{\ge 0}, i\in \{0,1,2\}$ such that following constraints can be satisfied:

The initial values of the variables x, y, z (in location $\iota$, source of edge i) are denoted $x_{-1}, y_{-1}, z_{-1}$ and are unconstrained. Hence we assume that the initial predicate on the variables $x_{-1}, y_{-1}, z_{-1}$ is $P_{-1} = True$. $P_0$ must be satisfied after taking i and letting time progress for $\delta _0 \ge 0$ time units, which is enforced by a constraint on the variables² $x_0, y_0, z_0$ that stand for the values of x, y, z after taking i; similarly $P_0 \wedge P_1$ must hold after $i.t_0$ and $P_0 \wedge P_1 \wedge P_2$ after $i.t_0.t_2$. Hence the set of timed words associated with $i.t_0.t_2$ is not empty iff $P_0 \wedge P_1 \wedge P_2$ is satisfiable. The timed language, $\mathcal{TL}(A_1)$, accepted by $A_1$ is the set of timed words associated with all the words w accepted by $A_1$ i.e., $\mathcal{TL}(A_1) = \cup _{w \in \mathcal{L}(A_1)} \tau (w)$.

The language emptiness problem is a standard problem in Timed Automata theory and is stated as follows [1]: “given a (Timed) Automaton A, is $\mathcal{TL}(A)$ empty?”. It is known that the emptiness problem is decidable for some classes of real-time programs (e.g., Timed Automata [1]), but undecidable for slightly more expressive classes (e.g., Stopwatch Automata [20]). It is usually possible to compute symbolic representations of sets of reachable valuations after a sequence of labels. However, to compute the set of reachable valuations we may need to explore an arbitrary and unbounded number of sequences. Hence only semi-algorithms exist to compute the set of reachable valuations. For instance, using PHAver to compute the set of reachable valuations for $A_1$ does not terminate (Table 1). To force termination, we can compute an over-approximation of the set of reachable valuations. Computing an over-approximation is sound (if we declare a timed language to be empty it is empty) but incomplete i.e., it may result in false positives (we declare a timed language non empty whereas it is empty). This is witnessed by the column “Uppaal” in Table 1 where Uppaal over-approximates sets of valuations in the stopwatch automaton with DBMs. After $i.t_0$, the over-approximation is $0 \le y \le x \wedge 0 \le z \le x$. This over-approximation intersects the guard $x - y \ge 1 \wedge z -y < 1$ of $t_2$ and $\ell _2$ is reachable but this is an artifact of the over-approximation.³

Table 1. Symbolic representation of reachable states after a sequence of instructions. Uppaal concludes that $\mathcal{TL}(A_1) \ne \varnothing$ due to the over-approximation using DBMs. PHAver does not terminate.

Neither Uppaal nor PHAver can prove that $\mathcal{TL}(A_1) = \varnothing$. The technique we introduce in this paper enables us to discover arbitrary abstractions and invariants that enable us to prove $\mathcal{TL}(A_1) = \varnothing$. Our method is a version of the Trace Abstraction Refinement (TAR) technique introduced in [17]. Let us demonstrate how the method works on the stopwatch automaton $A_1$:

• find a (untimed) word accepted by $A_1$. Let $w_1= i.t_0.t_2$ be such a word. We check whether $\tau (w_1) = \varnothing$ by encoding the corresponding associated timed traces as described by Eqs. ($P_{0}$)–($P_{2}$) and then check whether $P_0 \wedge P_1 \wedge P_2$ is satisfiable⁴. As $P_0 \wedge P_1 \wedge P_2$ is not satisfiable we have $\tau (w_1) = \varnothing$.

• from the proof that $P_0 \wedge P_1 \wedge P_2$ is not satisfiable, we can obtain an inductive interpolant that comprises of two predicates $I_0, I_1$ – one for each conjunction – over the clocks x, y, z. An example of inductive interpolant⁵ is $I_0 = x \le y$ and $I_1 = x - y \le z$. These predicates are invariants of any timed word of the untimed word $w_1$, and can be used to annotate $w_1$ with pre- and post-conditions (Eq. 1), which are Hoare triples of the form $\{P\} \ a \ \{Q\}$:

  $$\begin{aligned} \{ True \}&\quad i \quad \{I_0\} \quad t_0 \quad \{I_1\} \quad t_2 \quad \{ False \} \end{aligned}$$

  (1)
  $$\begin{aligned} \{ True \}&\quad i \quad \{I_0\} \quad t_0 \quad \pmb {\{I_1\}} \quad \pmb {(t_1)^*} \quad \pmb {\{I_1\} } \quad t_2 \quad \{ False \} \end{aligned}$$

  (2)

  We can also prove that $\{I_1\}\ (t_1)^*\ \{I_1\}$ is a valid Hoare triple and combined with Eq. 1 this gives Eq. 2. For each word $w \in i.t_0.(t_1)^*.t_2$, $\tau (w) = \varnothing$ and as $\mathcal{L}(A_1) \subseteq i.t_0.(t_1)^*.t_2$ we can conclude that $\mathcal{TL}(A_1) = \varnothing$.

3 Real-Time Programs

Our approach is general enough and applicable to a wide range of timed systems called real-time programs. As an example, timed, stopwatch, hybrid automata and time Petri nets are special cases of real-time programs.

In this section we define real-time programs. Real-time programs define the control flow of instructions, just as standard imperative programs do. The instructions can update variables by assigning new values to them. Each instruction has a semantics and together with the control flow this precisely defines the semantics of real-time programs.

Notations. A finite automaton over an alphabet $\varSigma$ is a tuple $\mathcal {A}=(Q,\iota ,\varSigma ,$ $\varDelta ,F)$ where Q is a finite set of locations s.t. $\iota \in Q$ is the initial location, $\varSigma$ is a finite alphabet of actions, $\varDelta \subseteq (Q\times \varSigma \times Q)$ is a finite transition relation, $F\subseteq Q$ is the set of accepting locations. A word $w = \alpha _0 . \alpha _1. \cdots . \alpha _n$ is a finite sequence of letters from $\varSigma$; we let $w[i] = \alpha _i$ the i-th letter, |w| be the length of w which is $n + 1$. Let $\epsilon$ be the empty word and $|\epsilon |=0$, $\varSigma ^*$ is the set of finite words over $\varSigma$. The language, $\mathcal{L}(\mathcal {A})$, accepted by $\mathcal {A}$ is defined in the usual manner as the set of words that can lead to $F$ from $\iota$.

Let V be a finite set of real-valued variables. A valuation is a function $\nu : V\rightarrow \mathbb {R}$. The set of valuations is $[V\rightarrow \mathbb {R}]$. We denote by $\beta (V)$ a set of constraints on the variables in $V$. Given $\varphi \in \beta (V)$, we let $\textit{Vars}(\varphi )$ be the set of free variables in $\varphi$. The truth value of a constraint $\varphi$ given a valuation $\nu$ is denoted by $\varphi (\nu )$ and we write $\nu \,\models \, \varphi$ when $\varphi (\nu ) = True$. We let ${\llbracket \varphi \rrbracket } = \{ \nu \mid \nu \,\models \, \varphi \}$. An update of the variables in $V$ is a binary relation $\mu \subseteq [V\rightarrow \mathbb {R}] \times [V\rightarrow \mathbb {R}]$. Given an update $\mu$ and a set of valuations $\mathcal {V}$, we let $\mu (\mathcal {V}) = \{ \nu ' \mid \exists \nu \in \mathcal {V}\text { and } (\nu ,\nu ') \in \mu \}$. We let $\mathcal{U}(V)$ be the set of updates on the variables in $V$. A rate $\rho$ is a function from $V$ to $\mathbb {Q}$ (rates can be negative), i.e., an element of $\mathbb {Q}^{V}$. We let $\mathcal {R}(V) \subseteq \mathbb {Q}^{V}$ be a set of valid rates – that is, rates that can be written (syntactically) as a predicate on an edge. Given a valuation $\nu$, a valid rate $\rho \in \mathbb {Q}(V)$ and a timestep $\delta \in \mathbb {R}_{\ge 0}$ the valuation $\nu + \rho \times \delta$ is defined by: $(\nu + \rho \times \delta )(v) = \nu (v) + \rho (v) \times \delta$ for $v \in V$.

Real-Time Instructions. Let $\mathcal{I}= \beta (V) \times \mathcal{U}(V) \times \mathcal {R}(V)$ be a countable set of instructions. Each $\alpha \in \mathcal{I}$ is a tuple $(\textit{guard, update, rates})$ denoted by $(\gamma _\alpha , \mu _\alpha , \rho _\alpha )$. Let $\nu : V\rightarrow \mathbb {R}$ and $\nu ' : V\rightarrow \mathbb {R}$ be two valuations. For each pair $(\alpha ,\delta ) \in \mathcal{I}\times \mathbb {R}_{\ge 0}$ we define the following transition relation:

The semantics of $\alpha \in \mathcal{I}$ is a mapping ${\llbracket \alpha \rrbracket } : [V \rightarrow \mathbb {R}] \rightarrow [V \rightarrow \mathbb {R}]$ that can be extended to sets of valuations as follows:

Let K be a set of valuations, $\alpha \in \mathcal{I}$ and $w \in \mathcal{I}^*$. We inductively define the post operator $\textit{Post}$ as follows:

$$\begin{aligned} \textit{Post}(K, \epsilon )&= K \\ \textit{Post}(K, \alpha .w)&= \textit{Post}({\llbracket \alpha \rrbracket }(K),w) \end{aligned}$$

The post operator extends to logical constraints $\varphi \in \beta (V)$ by defining $\textit{Post}(\varphi ,w) = \textit{Post}({\llbracket \varphi \rrbracket },w)$. In the sequel, we assume that, when $\varphi \in \beta (V)$,

then ${\llbracket \alpha \rrbracket }({\llbracket \varphi \rrbracket })$ is also definable as a constraint in $\beta (V)$. This inductively implies that $\textit{Post}(\varphi ,w)$ can also be expressed as a constraint in $\beta (V)$ for sequences of instructions $w \in \mathcal{I}^*$.

Timed Words and Feasible Words. A timed word (over alphabet $\mathcal{I}$) is a finite sequence $\sigma =(\alpha _0,\delta _0).(\alpha _1,\delta _1). \cdots .(\alpha _n,\delta _n)$ such that for each $0 \le i \le n$, $\delta _i \in \mathbb {R}_{\ge 0}$ and $\alpha _i \in \mathcal{I}$. The timed word $\sigma$ is feasible if and only if there exists a set of valuations $\{\nu _0,\dots ,\nu _{n+1}\} \subseteq [V\rightarrow \mathbb {R}]$ such that:

$$ \nu _0 \xrightarrow {~\alpha _0, \delta _0 ~} \nu _1 \xrightarrow {~\alpha _1, \delta _1 ~} \nu _2 \cdots \nu _n \xrightarrow {~\alpha _n, \delta _n ~} \nu _{n+1} \mathpunct . $$

We let $\textit{Unt}(\sigma ) = \alpha _0.\alpha _1.\cdots .\alpha _n$ be the untimed version of $\sigma$. We overload the term feasible as follows: an untimed word $w \in \mathcal{I}^*$ is feasible iff $w = \textit{Unt}(\sigma )$ for some feasible timed word $\sigma$.

Lemma 1

An untimed word $w \in \mathcal{I}^*$ is feasible iff $\textit{Post}( True ,w) \ne False$.

Proof

The lemma follows trivially from the inductive definition of $\textit{Post}$.    $\square$

Real-Time Programs. The specification of a real-time program decouples the control (e.g., for Timed Automata, the locations) and the data (the clocks). A real-time program is a pair $P=(A_P,{\llbracket \cdot \rrbracket })$ where $A_P$ is a finite automaton $A_P=(Q,\iota ,I, \varDelta , F)$ over the finite alphabet⁶ $I \subseteq \mathcal{I}$, $\varDelta$ defines the control-flow graph of the program and ${\llbracket \cdot \rrbracket }$ (as defined previously for $\mathcal{I}$) provides the semantics of each instruction. A timed word $\sigma$ is accepted by $P$ if and only if:

• 1. $\textit{Unt}(\sigma )$ is accepted by $A_P$ ($\textit{Unt}(\sigma ) \in \mathcal{L}(A_P)$) and

• 2. $\sigma$ is feasible.

Notice that the definition of feasibility of a timed word $\sigma$ is independent from the acceptance of $\textit{Unt}(\sigma )$ by $A_P$.

The timed language, $\mathcal{TL}(P)$, of a real-time program $P$ is the set of timed words accepted by $P$, i.e., $\sigma \in \mathcal{TL}(P)$ if and only if $\textit{Unt}(\sigma ) \in \mathcal{L}(A_P)$ and $\sigma$ is feasible.

Remark 1

We do not assume any particular values initially for the variables of a real-time program (the variables that appear in I). This is reflected by the definition of feasibility that only requires the existence of valuations without containing the initial one $\nu _0$. When specifying a real-time program, initial values can be set by regular instructions. This is similar to standard programs where the first instructions can set the values of some variables.

Timed Language Emptiness Problem. The (timed) language emptiness problem asks the following:

Given a real-time program $P$, is $\mathcal{TL}(P)$ empty?

Theorem 1

$\mathcal{TL}(P) \ne \varnothing$ iff $\exists w \in \mathcal{L}(A_P)$ such that $\textit{Post}( True ,w) \not \subseteq False$.

Proof

$\mathcal{TL}(P) \ne \varnothing$ iff there exists a feasible timed word $\sigma$ such that $\textit{Unt}(\sigma )$ is accepted by $A_P$. This is equivalent to the existence of a feasible word $w \in \mathcal{L}(A_P)$, and by Lemma 1, feasibility of w is equivalent to $\textit{Post}( True ,w) \not \subseteq False$.   $\square$

Useful Classes of Real-Time Programs. Timed Automata are a special case of real-time programs. The variables are called clocks. $\beta (V)$ is restricted to constraints on individual clocks or difference constraints generated by the grammar:

$$\begin{aligned} b_1, b_2 \,{:}{:}{=}\, True \mid False \mid x - y \bowtie k \mid x \bowtie k \mid b_1\wedge b_2 \end{aligned}$$

(3)

where $x, y\in V$, $k \in \mathbb {Q}_{\ge 0}$ and $\bowtie \,\in \{<,\le ,=,\ge ,>\}$ ⁷. We note that wlog. we omit location invariants as for the language emptiness problem, these can be implemented as guards. An update in $\mu \in \mathcal{U}(V)$ is defined by a set of clocks to be reset. Each pair $(\nu ,\nu ') \in \mu$ is such that $\nu '(x)=\nu (x)$ or $\nu '(x)=0$ for each $x \in V$. The valid rates are fixed to 1, and thus $\mathcal {R}(V) = \{1\}^V$.

Stopwatch Automata can also be defined as a special case of real-time programs. As defined in [9], Stopwatch Automata are Timed Automata extended with stopwatches which are clocks that can be stopped. $\beta (V)$ and $\mathcal{U}(V)$ are the same as for Timed Automata but the set of valid rates is defined by the functions of the form $\mathcal {R}(V) = \{0,1\}^V$ (the clock rates can be either 0 or 1). An example of a Stopwatch Automaton is given by the timed system $\mathcal {A}_1$ in Fig. 1.

As there exists syntactic translations (preserving reachability) that maps hybrid automata to stopwatch automata [9], and translations that map time Petri nets [5, 10] and extensions [7, 8] thereof to timed automata, it follows that time Petri nets and hybrid automata are also special cases of real-time programs. This shows that the method we present in the next section is applicable to wide range of timed systems.

Fig. 2.

Real-time program $P_2$

What is remarkable as well, is that it is not restricted to timed systems that have a finite number of discrete states but can also accommodate infinite discrete state spaces. For example, the automaton in Fig. 2 has two clocks x and y and an unbounded integer variable k. Even though k is unbounded, our technique discovers the invariant $y \ge k$ at location 1 which is over a real-time clock y and the integer variable k. It allows us to prove that $\mathcal{TL}(P_2) = \varnothing$.

4 Trace Abstraction Refinement for Real-Time Programs

In this section we propose a semi-algorithm to solve the language emptiness problem for real-time programs. The semi-algorithm is a version of the refinement of trace abstractions (TAR) approach [17] for timed systems.

Refinement of Trace Abstraction for Real-Time Programs. Figure 3 gives a precise description of the TAR semi-algorithm for real-time programs. This is the standard trace abstraction refinement semi-algorithm as introduced in [17] – we therefore omit theorems of completeness and soundness as these will be equivalent to the theorems in [17] and are proved in the exact same manner. The input to the semi-algorithm is a real-time program $P=(A_P, {\llbracket \cdot \rrbracket })$. An invariant of the semi-algorithm is that R is empty or contains only infeasible traces.

Fig. 3.

Trace abstraction refinement semi-algorithm for real-time programs

Initially the refinement R is the empty set. The semi-algorithm works as follows:

Step 1. :

Check whether all the (untimed) traces in $\mathcal{L}(A_P)$ are in R. If this is the case, $\mathcal{TL}(P)$ is empty and the semi-algorithm terminates. Otherwise, there is a sequence $w \in \mathcal{L}(A_P) \setminus R$, goto Step 2;

Step 2. :

If w is feasible i.e., there is a feasible timed word $\sigma$ such that $\textit{Unt}(\sigma )=w$, then $\sigma \in \mathcal{TL}(P)$ and $\mathcal{TL}(P) \ne \varnothing$ and the semi-algorithm terminates. Otherwise w is not feasible, goto Step 3;

Step 3. :

w is infeasible and given the reason for infeasibility we can construct a finite interpolant automaton, $\textit{IA}(w)$, that accepts w and other words that are infeasible for the same reason. How $\textit{IA}(w)$ is computed is addressed in the sequel. The automaton $\textit{IA}(w)$ is added to the previous refinement R and the semi-algorithm starts a new round at Step 1.

Checking Feasibility. Given a word $w \in \mathcal{I}^*$, we can check whether w is feasible by encoding the side-effects of each instruction in w, similar to a Static Single Assignment (SSA) form in programming languages.

Let us define a function for constructing such a constraint-system characterizing the feasibility of a given trace. We shall assume that constraints in $\beta (V)$ and updates in $\mathcal{U}(V)$ are syntactically defined. Let $P=(Q,q_0,\mathcal{I}, \varDelta , F)$ be a real-time program and $w\in \mathcal{I}^*$ be a word over $\mathcal{I}$. Let $V^n=\{x^n,x_\mu ^n\mid x\in V\}\cup \{\delta ^n\}$ be a set of variables extended with an index $n\in {\mathbb {N}_{\ge 0}}$. For a given constraint-system $\varphi \in \beta (V)$ write $\varphi _{[V/V^n]}$ for replacing all occurrences of V with their indexed occurrence in $V^n$ (implying that $\varphi _{[V/V^n]}\in \beta (V^n)$). We assume that the relation $\mu \in \mathcal{U}(V)$ is of SSA form, and let $\mu _{[V/(V^n,V^m)]}$ be the replacement of all occurrences of variables $x\in V$ with their indexes and sub-scripted occurrence in $V^n$ if x is assigned to and from $V^m$ if x is read from. As an example, $(v\leftarrow v+w)_{[V/(V^n,V^m)]}=v_\mu ^n\leftarrow v^m + w^m$ where $\leftarrow$ denotes assignment. Given this we can now recursively define the function $\textit{Enc}:\mathcal{I}^*\rightarrow \beta (\{V^n\mid 0\le n \le |w|\})$

$$\begin{aligned} \textit{Enc}(\epsilon ) =&True \\ \textit{Enc}(w.\alpha )=&\textit{Enc}(w) \wedge \delta ^n\ge 0 \wedge \varphi _{[V/V^{n-1}]} \wedge \delta ^n\ge 0 \wedge \mu _{[V/(V_\mu ^{n},V^{n-1})]}\\&{\wedge }\,\mathop \bigwedge \limits _{v\in V}v^{n}=v_\mu ^{n}+\rho (v)\times \delta ^n\text { where } n=|w|-1 \text { and }(\varphi ,\mu ,\rho )=\alpha \end{aligned}$$

The function $\textit{Enc}:\mathcal{I}^*\rightarrow \beta (V^{\mathbb {N}_{\ge 0}})$ constructs a constraint-system characterizing exactly the feasibility of a word w:

Lemma 2

A word w is feasible i.e., $\textit{Post}( True ,w) \not \subseteq False$ iff $\textit{Enc}(w)$ is satisfiable.

We shall frequently refer to such a constraints system $C=\textit{Enc}(w)$ for some word w where $|w|=n$ as a sequence of conjunctions $P_0\wedge \dots \wedge P_m\wedge \dots \wedge P_n=C$ where $P_m\in \beta (V^{m-1}\cup V^m)$ refers to the encoding of the m’th instruction, and we shall call such an element $P_m$ a predicate.

An example of an encoding for the real-time program $A_1$ (Fig. 1) is given by the predicates in Eqs. ($P_0$)–($P_2$). The variables $x_k, y_k, z_k$ denote the values of x, y, z after k steps (initially the variables can have arbitrary values). The sequence $w_1 = i.t_0.t_2$ is feasible iff $\textit{Enc}(w_1) = P_0 \wedge P_1 \wedge P_2$ is satisfiable.

From such a sequence we can use interpolating SMT-solvers to construct a sequence of craig-interpolants.

Construction of Interpolant Automata. When it is determined that a trace w is infeasible, we can easily discard such a single trace and continue searching. However, the power of the TAR method is to generalize the infeasibility of a single trace w into a family (regular set) of traces. This regular set of infeasible traces is computed from the reason of infeasibility of w and is formally specified by an interpolant automaton, $\textit{IA}(w)$. The reason for infeasibility itself has the form of an inductive interpolant.

Given a conjunctive formula $f = P_0\wedge \cdots \wedge P_m$, if f is unsatisfiable, an interpolating SMT-solver is capable of producing inductive arguments for the unsatisfiability reason. This argument is an inductive interpolant $I_0,\dots ,I_{m-1}$ s.t. for each $0 \le n \le m-1$, $I_n \wedge P_{n+1}$ implies $I_{n+1}$ (with $I_m = False$), and for each $0 \le n \le m-1$, the variables in $I_n$ appear in both $P_n$ and $P_{n+1}$.

One can intuitively think of each interpolant as a sufficient condition for infeasibility of the post-fix of the trace and this can be represented by a sequence of Hoare triples of the form $\{P\} \ a \ \{Q\}$:

$$\begin{aligned} \{ True \}&\quad a_0 \quad \{I_0\} \quad a_1 \quad \{I_1\} \quad \cdots \quad \{ I_{m-1} \} \quad a_m \quad \{ False \} \end{aligned}$$

Consider the real-time program $P_2$ of Fig. 2 and the two infeasible untimed words $w_1=i.t_0.t_2$ and $w_2=i.t_0.t_1.t_0.t_2$. The Hoare triples for $w_1$ and $w_2$ are given by Eq. 4 and 5 where the predicates are: $I_1= y \ge x \wedge (k=0)$, $I_2= y \ge k$, $I_3=y \ge x \wedge k \le 0$, $I_4=y \ge 1 \wedge k \le 0$, $I_5=y\ge k + x$, $I_6=y\ge k + 1$.

$$\begin{aligned} \{ True \}&\quad i \quad \{I_1\} \quad t_0 \quad \{ I_2 \} \quad t_2 \quad \{ False \} \end{aligned}$$

(4)

$$\begin{aligned} \{ True \}&\quad i \quad \{ I_3 \} \quad t_0 \quad \{I_4 \} \quad t_1 \quad \{ I_5\} \quad t_0 \quad \{I_6\} \quad t_2 \quad \{ False \} \end{aligned}$$

(5)

As can be seen in Eq. 5, the sequence contains two occurrences of $t_0$: this suggests that a loop occurs in the program, and this loop may be infeasible as well. Formally, because $\textit{Post}(I_6,t_1) \subseteq I_5$, any trace of the form $i.t_0.t_1.(t_0.t_1.t_0)^*.t_2$ is infeasible. This enables us to construct $\textit{IA}(w_2)$ as accepting the regular set of infeasible traces $i.t_0.t_1.(t_0.t_1.t_0)^*.t_2$. Overall, because $w_1$ is also infeasible, we obtain a refinement which is $\mathcal{L}(\textit{IA}(w_1)) \cup \mathcal{L}(\textit{IA}(w_2))$, Fig. 4.

Fig. 4.

Interpolant automaton for $\mathcal{L}(\textit{IA}(w_1)) \cup \mathcal{L}(\textit{IA}(w2))$.

Let us formalize the interpolant-automata construction. Given the interpolants $I_0,\dots I_k$ for the constraint-system $P_0\wedge \dots \wedge P_{k+1}=\textit{Enc}(w)$ for some word w where $k=|w|-1$ and given the automata description of our Real Time Program $\mathcal {A}=(Q,q_0,\varSigma ,\varDelta ,F)$, then we can construct an interpolant automaton $\mathcal {A}^I=(Q^I,q^I_0,\varSigma ^I,\varDelta ^I,F^I)$ s.t. $w\in \mathcal {L}(\mathcal {A}^I)$ and for all $w'\in \mathcal {L}(\mathcal {A}^I)$ we have that $w'$ is infeasible. Let $Q=\{ True , False ,I_0,\dots ,I_k\}$, $q_0= True$, $\varSigma ^I=\varSigma$, $F=\{ False \}$, then we let the transition-function be the largest transition-function satisfying the following.

• 1. $( True , w[0], I_0)\in \varDelta ^I$,

• 2. $(I_k, w[k], False )\in \varDelta ^I$,

• 3. $(I_{n-1}, w[n-1], l_{n})\in \varDelta ^I$ for $1< n \le k$, and

• 4. for each $1\le n,m\le k$, if $I_m\subset _{V} I_n$ then $(I_{n-1},w[n-1],I_m)\in \varDelta ^I$ where $\subset _V$ is subset-checking, modulo variable indexing.

The above conditions induce an algorithm $\textit{IA}$ for constructing interpolant automata from an untimed word w.

Theorem 2 (Interpolant Automata)

Let w be an infeasible word over $P$, then for all $w'\in \mathcal{L}(\textit{IA}(w))$, $w'$ is infeasible.

We can verify that the construction using rules 1–3 is correct as these come directly from the feasibility-check of the trace and the definition of interpolants.

The pumping-rule (rule 4) utilizes that if by firing some transition labeled $\alpha$ from some interpolant $I_{n-1}$ gives us a “stronger” argument for infeasibility than in $I_m$, then surely every sequence which is infeasible from $I_m$ is also infeasible from $I_{n-1}$ after firing $\alpha$.

Feasibility Beyond Timed Automata. Satisfiability can be checked with an SMT-solver (and decision procedures exist for useful theories). In the case of timed automata and stopwatch automata, the feasibility of a trace can be encoded as a linear program. The corresponding theory, Linear Real Arithmetic (LRA) is decidable and supported by most SMT-solvers. It is also possible to encode non-linear constraints (non-linear guards and assignments). In the latter cases, the SMT-solver may not be able to provide an answer to the SAT problem as non-linear theories are undecidable. However, we can still build on a semi-decision procedure of the SMT-solver, and if it provides an answer, get the status of a trace (feasible or not).

5 Parameter Synthesis for Real-Time Programs

In this section we show how to use the trace abstraction refinement semi-algorithm presented in Sect. 4 to synthesize good initial values for some of the program variables. Given a real-time program $P$, the objective is to determine a set of initial valuations $I \subseteq [V\rightarrow \mathbb {R}]$ such that, when we start the program in I, $P$ does not accept any timed word.

Given a constraint $I \in \beta (V)$, we define the associated assume guard-transformer for instructions that for a letter $\alpha =(\gamma ,\rho ,\mu )$ defines $\textit{Assume}(\alpha , I)=(\gamma ',\rho ,\mu )$ s.t. $\gamma =\gamma \wedge I$. Let $P=(Q, \iota , \mathcal{I}, \varDelta , F)$ be a real-time program. Then we can define the real-time program $\textit{Assume}(I).P=(Q, \iota , \mathcal{I}, (\varDelta \setminus \{(\iota ,i,q_0)\}) \cup \{(\iota ,\textit{Assume}(i,I),q_0)\}, F)$.

Safe Initial Set Problem. The safe initial state problem asks the following:

Given a real-time program $P$, is there $I \in \beta (V)$ s.t. $\mathcal{TL}(\textit{Assume}(I).P) = \varnothing$?

Semi-Algorithm for the Safe Initial State Problem. Let $w \in \mathcal{L}(P)$. When $\textit{Enc}(w)$ is satisfiable, we define the (existentially quantified) constraint $\exists \textit{Vars}(\textit{Enc}(w)) \setminus V_{-1}.\textit{Enc}(w)$ i.e., the projection of the set of solutions on the initial values of the variables. We let $\exists _i(w)$ be $\exists \textit{Vars}(\textit{Enc}(w)) \setminus V_{-1}.\textit{Enc}(w)$ with all the free occurrences of $x_{-1}$ replaced by x (remove index for each var). $\exists _i(w)$ is a constraint over the set of variables $V$ (and existential quantifiers)⁸.

The semi-algorithm in Fig. 5 works as follows: (1) initially $I = True$ (2) using the semi-algorithm from Fig. 3, test if $\mathcal{TL}(\textit{Assume}(I).P)$ is empty – if so $P$ does not accept any timed word when we start from ${\llbracket I \rrbracket }$ (3) Otherwise, there is a witness word $\sigma \in \mathcal{TL}(\textit{Assume}(I).P)$, implying that $I\wedge \textit{Enc}(\textit{Unt}(\sigma ))$ is satisfiable. We can then determine a sufficient condition $I'=\exists _i(\textit{Unt}(\sigma ))$ for the feasibility s.t. $(\lnot I')\wedge \textit{Enc}(\textit{Unt}(\sigma ))$ is unsatisfiable and use this to strengthen the constraint I (step 2).

If the semi-algorithm terminates, it computes exactly the set of parameters for which the system is not safe (I), captured formally by Theorem 3.

Theorem 3

If the semi-algorithm $SafeInit$ terminates and outputs I, then for any $I'\in \beta (V)$, $\mathcal{TL}(\textit{Assume}(I').P) = \varnothing$ if and only if $I' \subseteq I$.

Proof

( $\Longrightarrow$ ). Let us assume by contradiction that upon termination we have $\mathcal{TL}(\textit{Assume}(I).P)\ne \varnothing$. This violates the termination critirion of either Fig. 3 or 5.    $\square$

Proof

( $\Longleftarrow$ ). Let us assume by contradiction that upon termination there exists some $I'\ne \varnothing$ for which $I'\cap I=\varnothing$ and $\mathcal{TL}(\textit{Assume}(I').P)=\varnothing$. Then let us prove inductively that no such $I'$ can ever exist.

In the base-case in step 1, if the algorithm terminates, clearly $I'=\varnothing$ violating our requirements for the contradiction. For our contradiction to be valid, we must instead look at how we modify I in step 2. For $I'$ to be non-empty, the quantification over parameter-values for $\sigma$ must construct a larger-than-needed set of parameter value, i.e., that $I'\subseteq \lnot \exists _i\textit{Enc}(\textit{Unt}(\sigma ))$. This contradicts the definition of existential quantification. As we never over-approximate the parameter-set needed for the valuation in step 2, we can conclude that $I'$ cannot exist.   $\square$

Fig. 5.

Semi-algorithm $SafeInit$.

6 Experiments

We have conducted two sets of experiments, each testing the applicability of our proposed method (denoted by rttar) compared to state-of-the-art tools with specialized data-structures and algorithms for the given setting. All experiments were conducted on AMD Opteron 6376 Processors and limited to 1 hour of computation. The rttar tool uses the Uppaal parsing-library, but relies on Z3 [13] for the interpolant computation.

Verification of Timed and Stopwatch Automata. The real-time programs, $P_1$ of Fig. 1 and $P_2$ of Fig. 2 can be analyzed with our technique. The analysis (rttar algorithm, Fig. 3) terminates in two iterations for the program $P_1$, a stopwatch automaton. As emphasized in the introduction, neither Uppaal (over-approximation with DBMs) nor PHAver can provide the correct answer to reachability problem for $P_1$.

To prove that location 2 is unreachable in program $P_2$ requires to discover an invariant that mixes integers (discrete part of the state) and clocks (continuous part). Our technique successfully discovers the program invariants $I_5$ and $I_6$ (thanks to the interpolating SMT-solver). As a result the refinement depicted in Fig. 2 is constructed and as it contains $\mathcal{L}(A_{P_2})$ the refinement algorithm terminates and proves that 2 is not reachable. $A_{P_2}$ can only be analyzed in Uppaal with significant computational effort and bounded integers.

Robustness of Timed Automata. Another remarkable feature of our technique is that it can readily be used to check robustness of timed automata. In essence, checking robustness amounts to enlarging the guards of an TA A by an $\varepsilon > 0$. The resulting TA is $A_\varepsilon$. The automaton A is (safety) robust iff there is some $\varepsilon > 0$ such $\mathcal{TL}(A_{\epsilon }) = \varnothing$.

To address the robustness problem for a real-time program P, we use the semi-algorithm presented in Sect. 5 and reduce the robustness-checking problem to that of parameter-synthesis. Assuming P is robust⁹ i.e., there exists some $\epsilon >0$ such that $\mathcal{TL}(A_{\epsilon }) = \varnothing$ and the previous process terminates we can compute the largest set of parameters for which P is robust.

Table 2. Results for robustness analysis comparing rttar with symrob. Time is given in seconds. N/A indicates that symrob was unable to compute the robustness for the given model.

As Table 2 demonstrates, symrob [22] and rttar do not always agree on the results. Notably, since the TA M3 contains strict guards, symrob is unable to compute the robustness of it. Furthermore, symrob over-approximates $\epsilon$, an artifact of the so-called “loop-acceleration”-technique and the polyhedra-based algorithm. This can be observed in the modified model M3c, which is now analyzable by symrob, but differ in results compared to rttar. This is the same case with the model denoted a. We experimented with $\epsilon$-values to confirm that M3 is safe for all the values tested – while a is safe only for values tested respecting $\epsilon <\frac{1}{2}$. We can also see that our proposed method is significantly slower than symrob. As our tool is currently only a prototype with rudimentary state-space-reduction-techniques, this is to be expected.

Parametric Stopwatch Automata. In our last series of tests, we compare the rttar tool to Imitator [2] – the state-of-the-art parameter synthesis tool for reachability¹⁰. We shall here use the semi-algorithm is presented in Sect. 5 For the test-cases we use the gadget presented initially in Fig. 1, a few of the test-cases used in [3], as well as two modified version of Fischers Protocol, shown in Fig. 6. In the first version we replace the constants in the model with parameters. In the second version (marked by robust), we wish to compute an expression, that given an arbitrary upper and lower bound yields the robustness of the system – in the same style as the experiments presented in Sect. 6, but here for arbitrary guard-values.

As illustrated by Table 3 the performance of rttar is slower than Imitator when Imitatoris able to compute the results. On the other hand, when using Imitator to verify our motivating example from Fig. 1, we observe that Imitator never terminates, due to the divergence of the polyhedra-computation. This is the effect illustrated in Table 1.

When trying to synthesize the parameters for Fischers algorithm, in all cases, Imitator times out and never computes a result. For both two and four processes in Fischers algorithm, our tool detects that the system is safe if and only if $a< 0 \vee b < 0 \vee b - a > 0$. Notice that $a< 0 \vee b < 0$ is a trivial constraint preventing the system from doing anything. The constraint $b - a > 0$ is the only useful one. Our technique provides a formal proof that the algorithm is correct for $b -a >0$.

In the same manner, our technique can compute the most general constraint ensuring that Fischers algorithm is robust.

Table 3. Results for parameter-synthesis comparing rttar with Imitator. Time is given in seconds. DNF marks that the tool did not complete the computation within an hour.

Fig. 6.

A Uppaal template for a single process in Fischers Algorithm. The variables e, a and b are parameters for $\epsilon$, lower and upper bounds for clock-values respectively.

The result of rttar algorithm is that the system is robust iff $\epsilon \le 0 \vee a< 0 \vee b < 0\vee b - a - 2\epsilon > 0$ – which for $\epsilon =0$ (modulo the initial non-zero constraint on $\epsilon$) reduces to the constraint-system obtained in the non-robust case.

7 Conclusion

We have proposed a version of the trace abstraction refinement approach to real-time programs. We have demonstrated that our semi-algorithm can be used to solve the reachability problem for instances which are not solvable by state-of-the-art analysis tools.

Our algorithms can handle the general class of real-time programs that comprises of classical models for real-time systems including timed automata, stopwatch automata, hybrid automata and time(d) Petri nets.

As demonstrated in Sect. 6, our tool is capable of solving instances of reachability problems problems, robustness, parameter synthesis, that current tools are incapable of handling.

For future work we would like to improve the scalability of the proposed method, utilizing well known techniques such as extrapolations, partial order reduction and compositional verification. Furthermore, we would like to extend our approach from reachability to more expressive temporal logics.