Verification and Parameter Synthesis for Real-Time Programs using Refinement of Trace Abstraction¹¹1A preliminary version of this work appeared in [13].

Reasoning about quantitative properties of programs requires extended modeling features like real-time clocks. Timed Automata [2] (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 [5]. Extending TA, e.g., with the ability to stop and resume clocks (stopwatches), leads to undecidability of the reachability problem [14, 29] which is the basic verification problem. As a result, semi-algorithms have been designed to verify extended classes of TA e.g., hybrid automata, and are implemented in a number of dedicated tools [23, 25, 28]. However, a common difficulty with the analysis of quantitative properties of timed automata and extensions thereof is that specialized 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.

The trace abstraction refinement (TAR) technique was proposed by Heizmann et al. [26, 27]. Wang et al. [35] 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. Moreover, 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.

Several works have investigated CEGAR techniques in both timed and hybrid settings [1, 21, 24, 34]. The CEGAR technique has also been extended to parameter-synthesis [24]. As proved by Heizmann et al. [26], such methods are special cases of the TAR framework.

The IC3 [10] verification approach has also been deployed for the verification of hybrid systems [9] but relies on a fix-point computation over a combined encoding of the transition-function, rather than a trace-subtraction approach. IC3 approaches and the likes have also been used for parameter synthesis [7, 9, 18]. While similar fundamental techniques are leveraged in these approaches (e.g. [7] utilizes Fourier-Motzkin-elimination), we note that our refinement method (TAR) is radically different in nature. IC3 is an iterative fix-point computation over an up-front and complete encoding of the transition-function.

Since the publication of a preliminary version of this paper [13], Kafle et al. [31] have demonstrated a novel method of parameter synthesis for timed systems via Constrained Horn Clauses (CHC). While their approach shows promising results for the Fischers parameter synthesis examples from [13], it currently relies on manual translation of a given problem into CHC format, hindering its applicability to large systems.

As mentioned earlier, our technique allows for a unique and logical (predicates) representation of sets of states accross different models (timed, hybrid automata) and problems (reachability, robustness, parameter synthesis), which is in contrast to state-of-the-art tools such as Uppaal [5], SpaceEx [25], HyTech [28], PHAver [23], verifix [32], symrob [33] and Imitator [3] that rely on special-purpose polyhedra libraries to realize their computation.

We propose a new technique which is radically different to previous approaches and leverages the power of SMT-solvers to discover non-trivial invariants for a large class of real-time systems including 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 state-space. 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. For instance they can express constraints that combine discrete and continuous variables of the system. This enables us to use our algorithm on non-decidable classes like stopwatch automata, and successfully (i.e., the algorithm terminates) check instances of these classes. A simple example is discussed in Section 2.

We propose a variant of the trace abstractions refinement (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.

This paper is an extended version of [13] in which we first introduced TAR for real-time programs. In this extended version, we provide a comprehensive introduction illustrated by more examples, extensions of the original algorithms from [13] and the proofs of theorems and lemmas.

A sequence of program instructions $w=a_{\_}0.a_{\_}1.\cdots.a_{\_}n\in\mathcal{L}(A_{\_}1)$ defines a (possibly empty) set of timed words, $\tau(w)$, of the form $(a_{\_}0,\delta_{\_}0).\cdots$ $(a_{\_}n,\delta_{\_}n)$ where $\delta_{\_}i\geq 0,i\in[0..n]$ is the time elapsed between two discrete transitions. 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}_{\_}{\geq 0},i\in\{0,1,2\}$ such that the following constraints (predicates that define that each transition can be fired after $\delta_{\_}i$ time units) can be satisfied²²2We assume the program starts in $\iota$ and all the variables are initially zero.:

These constraints encode the following semantics: $i$ is taken after $\delta_{\_}0$ time units and at that time $x,y,z$ are equal to $\delta_{\_}0$ and hence $x_{\_}0,y_{\_}0,z_{\_}0$ are the values of the variables when location $\ell_{\_}0$ is entered. The program remains in $\ell_{\_}0$ for $\delta_{\_}1$ time units. When $t_{\_}0$ is taken after $\delta_{\_}1$ time units, the values of $x,y,z$ is given by $x_{\_}1,y_{\_}1,z_{\_}1$. Finally the program remains $\delta_{\_}2$ time units in $\ell_{\_}1$ and $t_{\_}2$ is taken to reach $\ell_{\_}2$ which is the end of the program. It follows that the program can execute $i.t_{\_}0.t_{\_}2$ (or in other words, $i.t_{\_}0.t_{\_}2$ is feasible) if and only if we can find $\delta_{\_}0,\delta_{\_}1,\delta_{\_}2$ such that $C_{\_}0\wedge C_{\_}1\wedge C_{\_}2$ is satisfiable. Hence the set of timed words associated with $i.t_{\_}0.t_{\_}2$ is not empty iff $C_{\_}0\wedge C_{\_}1\wedge C_{\_}2$ is satisfiable.

The timed language, ${\cal TL}(P_{\_}1)$, accepted by $P_{\_}1$ is the set of timed words associated with all the (untimed) words $w$ accepted by $A_{\_}1$ i.e., ${\cal TL}(P_{\_}1)=\cup_{\_}{w\in{\cal L}(A_{\_}1)}\tau(w)$.

The language emptiness problem is a standard problem in Timed Automata theory [2] and is stated as follows for real-time programs:

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

It is known that the emptiness problem is decidable for some classes of real-time programs like Timed Automata [2], but undecidable for more expressive classes like Stopwatch Automata [29]. It is usually possible to compute symbolic representations of sets of reachable valuations after a sequence of transitions. 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 $P_{\_}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 an over-approximation of a timed language to be empty the timed language 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 program $P_{\_}1$ using DBMs. After $i.t_{\_}0$, the over-approximation is $0\leq y\leq x\wedge 0\leq z\leq x$ (this is the smallest DBMs that contains the actual set of valuations reachable after $i.t_{\_}0$). This over-approximation intersects the guard $x-y\geq 1\wedge z<1$ of $t_{\_}2$ which enables $t_{\_}2$. Using this over-approximate set of valuations we would declare that $\ell_{\_}2$ is reachable in $P_{\_}1$ but this is an artifact of the over-approximation.³³3Uppaal terminates with the result “the language may not be empty”. Neither Uppaal nor PHAver can prove that ${\cal TL}(P_{\_}1)=\varnothing$.

The technique we introduce can discover arbitrary abstractions and invariants that enable us to prove ${\cal TL}(P_{\_}1)=\varnothing$. Our method is a version of the trace abstraction refinement (TAR) technique introduced in [26] and is depicted in Figure 2.

• •

  we initially let $L={\cal L}(CFG(P_{\_}1))$. Since $w_{\_}1=i.t_{\_}0.t_{\_}2\in{\cal L}(CFG(P_{\_}1))$ and thus $w_{\_}1\in L$ the check $L=\varnothing$ fails. We therefore check whether $\tau(w_{\_}1)=\varnothing$ which can be done by encoding the corresponding set of timed traces as described by Equations ($C_{\_}0$)–($C_{\_}2$) and then check whether $C_{\_}0\wedge C_{\_}1\wedge C_{\_}2$ is satisfiable (e.g., using an SMT-solver and the theory of Linear Real Arithmetic). $C_{\_}0\wedge C_{\_}1\wedge C_{\_}2$ is not satisfiable and this establishes $\tau(w_{\_}1)=\varnothing$.

• •

  from the proof that $C_{\_}0\wedge C_{\_}1\wedge C_{\_}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 variables $x,y,z$. An example of an inductive interpolant⁵⁵5This is the pair returned by Z3 for $C_{\_}0\wedge C_{\_}1\wedge C_{\_}2$. is $I_{\_}0=x\leq y$ and $I_{\_}1=x-y\leq z$. These predicates are invariants of any timed word of the untimed word $w_{\_}1$, and can be used to annotate the sequence of transitions $w_{\_}1$ with pre- and post-conditions (Equation 1), which are Hoare triples of the form $\{C\}\ a\ \{D\}$:

  $$\{\mathit{True}\}\quad i\quad\{I_{\_}0\}\quad t_{\_}0\quad\{I_{\_}1\}\quad t_{\_}2\quad\{\mathit{False}\}$$

  (1)

  A triple $\{C\}\ a\ \{D\}$ is valid if whenever we start in a state $s$ satisfying $C$, and execute instruction $a$, the resulting new state $s^{\prime}$ is in $D$. $\{C\}\ a\ \{\mathit{False}\}$ means that no state exists after executing $a$ from $C$, i.e., the trace $a$ is infeasible. The inductiveness of the interpolants is due to the fact that each triple $\{C\}\ a\ \{D\}$ in the sequence (1) is a valid Hoare triple. Hoare triples (and validity) generalise to sequences of instructions $\sigma$ in the form $\{C\}\ \sigma\ \{D\}$.

  Because we can also prove that $\{I_{\_}1\}\ (t_{\_}1)^{\ast}\ \{I_{\_}1\}$ is a valid Hoare triple, if we combine this fact with Equation 1 we obtain a regular set of traces annotated with pre/post-conditions as per Equation 2.

  $$\{\mathit{True}\}\quad i\quad\{I_{\_}0\}\quad t_{\_}0\quad\boldsymbol{\{I_{\_}1\}}\quad\boldsymbol{(t_{\_}1)^{\ast}}\quad\boldsymbol{\{I_{\_}1\}}\quad t_{\_}2\quad\{\mathit{False}\}$$

  (2)

  This implies that the regular set of traces $i.t_{\_}0.(t_{\_}1)^{\ast}.t_{\_}2$ does not have any associated timed traces: for each word $w\in i.t_{\_}0.(t_{\_}1)^{\ast}.t_{\_}2$, $\tau(w)=\varnothing$ and as ${\cal L}(CFG(P_{\_}1))\subseteq i.t_{\_}0.(t_{\_}1)^{\ast}.t_{\_}2$ we can conclude that ${\cal TL}(A_{\_}1)=\varnothing$.

The following example (Figure 3) illustrates how extensions of timed automata with constraints that mix discrete and real variables can be analyzed. The real-time program $P_{\_}2$ (Figure 3) is given by the CFG (left) and the instructions⁶⁶6The rates table is omitted as all the variables are clocks with rate $1$. (right): it specifies a timed automaton with $2$ clocks $x,y$ (real variables) and one integer variable $i$.

This is an extended version of timed automata as the constraint $y<i$ mixes integer and real variables (clocks) and this is not permitted in the standard definition of timed automata. Initially all the variables are set to $0$. The objective is to prove that location $\ell_{\_}1$ is unreachable and thus that ${\cal TL}(P_{\_}2)=\varnothing$. Note that Uppaal does allow this specification but is unable to prove that $\ell_{\_}1$ is unreachable because $i$ is unbounded.

Our method is able to discover invariants that mix integer and real variables and can prove that $\ell_{\_}1$ is unreachable as follows:

1. 1.

   the first iteration of the TAR algorithm starts with $L={\cal L}(CFG(P_{\_}2))$. The check $L=\varnothing$ is negative as $w_{\_}1=t_{\_}0.t_{\_}2\in L$. However every timed word in $\tau(w_{\_}1)$ must satisfy the following constraints that correspond to taking $t_{\_}0$ and then $t_{\_}2$:

   	$\displaystyle\underbrace{x_{\_}0=y_{\_}0=\delta_{\_}0\wedge\delta_{\_}0\geq 0\wedge i_{\_}0=0}_{\_}{\text{Time elapsing $\delta_{\_}0$ in $\iota$}}\,\wedge\underbrace{x_{\_}0\geq 1}_{\_}{\text{Guard of $t_{\_}0$}}$			($C^{\prime}_{\_}0$)
   	$\displaystyle\underbrace{x_{\_}1=x_{\_}0+\delta_{\_}1\wedge y_{\_}1=y_{\_}0+\delta_{\_}1\wedge i_{\_}1=i_{\_}0\wedge\delta_{\_}1\geq 0}_{\_}{\text{Update of $t_{\_}0$ and time elapsing $\delta_{\_}1$ in $\ell_{\_}0$}}\,\wedge\underbrace{y_{\_}1<i_{\_}1}_{\_}{\text{Guard of $t_{\_}2$}}$			($C^{\prime}_{\_}1$)

   $C^{\prime}_{\_}0\wedge C^{\prime}_{\_}1$ is not satisfiable and hence ${\cal TL}(t_{\_}0.t_{\_}2)=\varnothing$ and thus we can safely remove $w_{\_}1$ from $L$. We can extract interpolants from the proof of unsatisfiability of $C^{\prime}_{\_}0\wedge C^{\prime}_{\_}1$ and we establish the following sequence of valid Hoare triples:

   $$\{x=y=i=0\}\quad t_{\_}0\quad\{x=y\wedge x\geq i\}\quad t_{\_}2\quad\{\mathit{False}\}$$

   (3)

2. 2.

   the second iteration of the TAR algorithm starts with an updated $L={\cal L}(CFG(P_{\_}2))\setminus\{w_{\_}1\}$. Again $L$ is not empty and for instance $w_{\_}2=t_{\_}0.t_{\_}1.t_{\_}0.t_{\_}2$ is in $L$. The encoding for checking the emptiness of $\tau(w_{\_}2)$ is:

   	$\displaystyle\underbrace{x_{\_}0=y_{\_}0=\delta_{\_}0\wedge\delta_{\_}0\geq 0\wedge i_{\_}0=0}_{\_}{\text{Time elapsing $\delta_{\_}0$ in $\iota$}}\,\wedge\underbrace{x_{\_}0\geq 1}_{\_}{\text{Guard of $t_{\_}0$}}$			($C^{\prime\prime}_{\_}0$)
   	$\displaystyle\underbrace{x_{\_}1=x_{\_}0+\delta_{\_}1\wedge y_{\_}1=y_{\_}0+\delta_{\_}1\wedge i_{\_}1=i_{\_}0\wedge\delta_{\_}1\geq 0}_{\_}{\text{Update of $t_{\_}0$ and time elspsing $\delta_{\_}1$ in $\ell_{\_}0$}}\wedge\underbrace{\mathit{True}}_{\_}{\text{Guard of $t_{\_}1$}}$			($C^{\prime\prime}_{\_}1$)
   	$\displaystyle\underbrace{x_{\_}2=0+\delta_{\_}2\wedge y_{\_}2=y_{\_}1+\delta_{\_}2\wedge i_{\_}2=i_{\_}1+1\wedge\delta_{\_}2\geq 0}_{\_}{\text{Time elapsing $\delta_{\_}2$ in $\iota$}}\wedge\underbrace{x_{\_}2\geq 1}_{\_}{\text{Guard of $t_{\_}0$}}$			($C^{\prime\prime}_{\_}2$)
   	$\displaystyle\underbrace{x_{\_}3=x_{\_}2+\delta_{\_}3\wedge y_{\_}3=y_{\_}2+\delta_{\_}3\wedge i_{\_}3=i_{\_}2\wedge\delta_{\_}3\geq 0}_{\_}{\text{Time elapsing $\delta_{\_}3$ in $\ell_{\_}0$}}\wedge\underbrace{y_{\_}3<i_{\_}3}_{\_}{\text{Guard of $t_{\_}2$}}$			($C^{\prime\prime}_{\_}3$)

   $C^{\prime\prime}_{\_}0\wedge C^{\prime\prime}_{\_}1\wedge C^{\prime\prime}_{\_}2\wedge C^{\prime\prime}_{\_}3$ is unsatisfiable and hence ${\cal TL}(t_{\_}0.t_{\_}1.t_{\_}0.t_{\_}2)=\varnothing$. We can extract interpolants from the proof of unsatisfiability and we establish the following sequence of valid Hoare triples.

   $$\{x=y=i=0\}\quad t_{\_}0\quad\{y\geq i\}\quad t_{\_}1.t_{\_}0\quad\{y\geq i\}\quad t_{\_}2\quad\{\mathit{False}\}$$

   (4)

   As can be seen as $\{y\geq i\}\ t_{\_}1.t_{\_}0\ \{y\geq i\}$ holds we can generalize this sequence to an arbitrary number of iterations of $t_{\_}0.t_{\_}1$:

   $$\{x=y=i=0\}\quad t_{\_}0\quad\boldsymbol{\{y\geq i\}}\quad\boldsymbol{(t_{\_}1.t_{\_}0)^{+}}\quad\boldsymbol{\{y\geq i\}}\quad t_{\_}2\quad\{\mathit{False}\}$$

   (5)

   which entails that ${\cal TL}(t_{\_}0.(t_{\_}1.t_{\_}0)^{+}.t_{\_}2)=\varnothing$. This implies that we can remove $t_{\_}0.(t_{\_}1.t_{\_}0)^{+}.t_{\_}2$ from $L$.

3. 3.

   observe that $L=\varnothing$ in the next iteration of TAR as ${\cal L}(CFG(P_{\_}2))\setminus(\{t_{\_}0.t_{\_}2\}\cup t_{\_}0.(t_{\_}1.t_{\_}0)^{+}.t_{\_}2)=\varnothing$ given that ${\cal L}(CFG(P_{\_}2))=t_{\_}0.(t_{\_}1.t_{\_}0)^{\ast}.t_{\_}2$. We have thus proved that ${\cal TL}(P_{\_}2)=\varnothing$ as any word of instructions in ${\cal L}(CFG(P_{\_}2))$ induces an infeasible trace and the algorithm terminates.

In the rest of the paper, we provide a formal development of the methods we have introduced so far.