We present and evaluate a straightforward method of representing finite runs of a parametric timed automaton (PTA) by means of formulae accepted by satisfiability modulo theories (SMT)-solvers. Our method is applied to the problem of parametric reachability, i.e., the synthesis of a set of the parameter substitutions under which a state satisfying a given property is reachable. While the problem of parametric reachability is not decidable in general, we provide algorithms for underapproximation of the solution to this problem for a certain class of PTA, namely for the lower/upper bound automata.
Model checking of real-time systems (RTS), performed by the analysis of their
models is a very important subject of research. This is highly motivated by an
increasing demand to verify safety critical systems, i.e., time-dependent systems,
failure of which could cause dramatic consequences for both people and
hardware. These systems include robotic surgery machines, nuclear reactor control
systems, railway signalling, breaking systems, air traffic control systems, flight
planning systems, rocket range launch safety systems, and many others. Humans
already benefit a lot from a variety of real-time systems, being often unaware of
this. Parametric model checking [
Timed automata (TA) [
In [
From the practical point of view the synthesis of all the parameter valuations is usually not needed: an analyst would typically be satisfied with a possibility of obtaining just a part of them. The direct analysis of parametric region graph is not feasible due to its typically large size, therefore the new methods of unwinding of the state space are needed. To this end, in this paper we offer a direct translation from an unwinding of the the concrete model of an L/U automaton to an SMT instance. This allows for synthesizing a subset of the parameter valuations for which an automaton satisfies some reachability property.
The rest of the paper is organized as follows. In the next section we briefly present the theory of parametric timed automata and formulate the task of parametric synthesis. In Section 3 we present how to encode all the finite runs of a 1 IEEE Computer Society. IEEE Standard for a High Performance Serial Bus. Std 1394-1995, 1996. given length as an SMT formula, and in Section 4 the algorithm for a state space exploration and a parameter synthesis for L/U automata is presented. Section 5 contains the preliminary evaluation of our method, as applied to two benchmarks: Fischer’s Mutual Exclusion Protocol and a version of Generic Timed Pipeline Paradigm. We conclude with a brief discussion in Section 5. 2
In this section we introduce all the main notions and define timed automata, parametric timed automata, and L/U automata.
Parametric timed automata, to be defined later, employ two sets of variables: the set X = {x1, . . . , xn} of real time variables, called clocks, and the set P = {p1, . . . , pm} of integer variables, called parameters. Both types of the variables are used in the clock constraints of parametric timed automata.
The clock constraints are built using linear expressions, i.e., expressions of the form Pm
i=1 ti · pi + t0, where ti ∈ Z. Clocks or differences of clocks compared with linear expressions, formally, the expressions of the form xi ≺ e or xi − xj ≺ e, where i 6= j, ≺∈ {≤, <} and e is a linear expression, are called simple guards. The conjunctions of simple guards are called guards. By G we denote the set of all guards. By G0 we mean the subset of G consisting of the guards built only of the simple guards of type xi ≺ e, where xi ∈ X and ≺∈ {≤, <}.
The clocks range over the nonnegative reals (R≥0) while the parameters range over the naturals (N, including 0). The function υ : P → N is called a parameter valuation and ω : X → R≥0 is called a clock valuation. Sometimes it is convenient to perceive υ and ω as points in, respectively, Nm and R≥0 n .
The value obtained by substituting the parameters in a linear expression e according to the parameter valuation υ is denoted by e[υ]. If ω(xi) − ω(xj ) ≺ e[v] (ω(xi) ≺ e[v]) holds, then we write ω |=υ xi − xj ≺ e (resp., ω |=υ xi ≺ e). This notion is naturally extended to the guards.
Two operations can be executed on the clocks: incrementation and reset. Let ω be a clock valuation and δ ∈ R, then by ω + δ we denote such a clock valuation that (ω + δ)(xi) = ω(xi) + δ for all 1 ≤ i ≤ n. A set of the expressions of the form xi := bi, where bi ∈ N, and 1 ≤ i ≤ n is called a reset, and the set of all resets is denoted by R. Let ω be a clock valuation and r be a reset, then by ω[r] we denote such a clock valuation that ω[r](xi) = bi if xi := bi ∈ r, and ω[r](xi) = ω(xi) otherwise. Intuitively, resetting a clock valuation amounts to setting the selected clocks to some fixed values, while leaving the remaining clocks intact. The initial clock valuation ω0 satisfies ω0(xi) = 0 for all xi ∈ X. 2.1
Timed automata [
A transition (q, a, g, r, q0) ∈→ is typicaly denoted by q a→,g,r q0.
Notice that the co-domain of the invariant function is the conjunction of upper
bounds on clocks. This assumption is taken from [
The concrete semantics of a parametric timed automaton under a parameter valuation υ is defined in the form of a labelled transition system. Definition 2 (Concrete semantics). Let A = hQ, l0, A, X, P, →, Ii be a parametric timed automaton and υ be a parameter valuation. The labelled transition system for A under υ is defined as the tuple JAKυ = hS, s0, R≥0 ∪ A, →di, where: – S = {(l, ω) | l ∈ Q, and ω is a clock valuation such that ω |=υ I(l)}, – s0 = (l0, ω0) (we assume that ω0 |=υ I(l0)), – Let (l, ω), (l0, ω0) ∈ S. The transition relation →d⊆ S ×S is defined as follows: • if d ∈ R≥0, then (l, ω) →d (l0, ω0) iff (l = l0 and ω0 = ω + d), • if d ∈ A, then (l, ω) →d (l0, ω0) iff l d→,g,r l0, for some g ∈ G, r ∈ R, where ω |=υ g, and ω0 = ω[r].
The elements of S are called the concrete states of JAKυ.
After substituting the parameters in A according to a parameter valuation υ
we obtain the timed automaton, denoted by Aυ. The concrete semantics of
Aυ is usually denoted by JAυK and it is straightforward [
For k ∈ N by a k-run ρk in ρk = s0 →d0 s0 a→ct1 s1 →d1 s0 actJ2A. K.υ. dwke−1mse0ka−n1a sequence of states and transitions: 0 1 → → a→ctk sk →dk s0k, where di ∈ R≥0 and acti ∈ A for all 0 ≤ i ≤ k. By a run we mean any k-run for k ∈ N. We say that k is the length of ρk and s0k is k–reachable in JAKυ. 2.2
The original definition of parametric timed automata [
Following [
φ = l | xi ≺ b | xi − xj ≺ b | φ ∧ φ | ¬φ, where l ∈ Q, xi, xj ∈ X, ≺∈ {≤, <} and b ∈ N.
We also refer to a state formula as to a property. Let υ be a parameter valuation, (l, ω) ∈ JAKυ, and let φ, ψ be state formulae. We define the validity of a state formula in a global states, denoted (l, ω) |= φ, inductively as follows: – (l, ω) |= l0 iff l = l0, – (l, ω) |= xi ≺ b iff ω |=υ xi ≺ b, and (l, ω) |= xi − xj ≺ b iff ω |=υ xi − xj ≺ b, – (l, ω) |= φ ∧ ψ iff (l, ω) |= φ and (l, ω) |= ψ, – (l, ω) |= ¬φ iff not (l, ω) |= φ.
Let υ be a parameter valuation and φ be a state formula. Let k ∈ N, dj ∈ R≥0 and actj ∈ A for all 1 ≤ j ≤ k. Let ρk = s0 →d0 s00 a→ct1 s1 →d1 s01 a→ct2 . . . d→k−1 s0k−1 → actk sk →dk s0k be a k-run in JAKυ. If for some k ∈ N there exists a run ρk in JAKυ such that s0k |= φ, then we say that a state satisfying φ is reachable in A under υ and write JAKυ |= EF φ. The EF modality originates from Computation Tree Logic (CTL), where EF φ stands for “there exists a path such that eventually φ holds”.
The task of parametric reachability, otherwise called the parameter synthesis problem, is formulated as follows.
Let A be parametric timed automaton and let φ be a state formula.
Automatically describe the set Γ (A, φ) = {υ | JAKυ |= EF φ}.
As mentioned earlier, there is no decision procedure for checking whether Γ (A, φ) is empty or contains all the parameter valuations, therefore we can not expect to be able to fully solve the parameter synthesis problem, at least in the general case. 2.3
Hune et al. have identified in [
In what follows if f is a function and B a subset of its domain, then f|B stands for the restriction of f to B. Definition 4. A lower/upper bound automaton is a parametric timed automaton A = hQ, l0, A, X, P, →, Ii satisfying the following conditions – P = L ∪ U , where L = {λ1, . . . , λl}, U = {μ1, . . . , μu}, and L ∩ U = ∅. – Each linear expression in the guards or the invariants of A can be written in form Pli=1 li · λi + Pju=1 uj · μj + t0, where li, uj , t0 ∈ Z and li ≤ 0, uj ≥ 0 for all 1 ≤ i ≤ l and 1 ≤ j ≤ u.
The elements of L are called the lower parameters while the elements of U are called the upper parameters.
Intuitively, in an L/U automaton the clock constraints can be uniformly relaxed by decreasing the values assigned to the lower parameters and increasing the values assigned to the upper parameters.
Let A be an L/U automaton and υ be a parameter valuation. Define λ = υ|L and μ = υ|U . If υ0 is also a valuation of the parameters, λ0 = υ0|L, μ0 = υ0|U , and ∀λi∈Lλ0(λi) ≤ λ(λi) and ∀μj∈U μ(μj ) ≤ μ0(μj ), then we write υ ≤ υ0.
When it is convenient to define υ in terms of of λ and μ, we write υ = (λ, μ).
Proposition 1 ([
Assume that A is an L/U automaton. From the above lemma it follows that the
problem of the emptiness of Γ (A, φ) can be reduced to the problem of
reachability of a state satisfying φ in the automaton obtained from A by substituting
lower parameters with 0 and removing each guard or invariant containing at least
one upper parameter. The latter, in terms of [
The idea of encoding of system’s behavior using the translation to propositional
formulae originates from [
SMT-solvers extend the capabilities of SAT-solvers by allowing for formulae
of the first order over several built-in theories as an input. In our considerations,
we use SMT-solvers to obtain the satisfiability and example models (valuations
of the parameters) for formulae expressed using boolean variables and operators
together with real-valued variables, linear arithmetic operators and relations. As
we have decided to make the translation as straightforward as possible, in this
experimental phase we have chosen to use SMT-lib ver. 2.0 [
Let A = hQ, l0, A, X, P, →, Ii be a parametric timed automaton. In this section we show how to encode, for a given k ∈ N, all the k-runs of Aυ for all the parameter valuations υ, as the formula acceptable by SMT solvers such as CVC3. We start with the description of the sorts (types), the variables, and the additional predicates used. 3.1
We encode the locations of A by means of enumerating them using propositional expressions. For each i ∈ N let BVi = {bv1i, bv2i, . . . , bvdilog|Q|e} be a set of propositional variables. Let BE i denote the set of all the propositional formulae over BVi. It is straightforward to notice for each i ∈ N we can define the function loc enci : Q → BE i assigning to each of the locations from Q the conjunction of the literals (variables or their negations) from BVi such that loc enci(l) ∧ loc encj (l0) is false iff i 6= j or l 6= l0. Intuitively, for l ∈ Q and i ∈ N, the formula loc enci(l) can be interpreted as an encoding of the location l at the i–th step (i ≤ k) of the k-runs, using variables from BVi.
Recall that X = {x1, x2, . . . , xn} is a set of the clocks. For each i ∈ N let Xi = {xi1, xi2, . . . , xin} be a set of real variables, where Xi ∩ Xj = ∅ for i 6= j, and similarly, let T = {t0, t1, . . .} be a set of real variables. As previously, the variables from Xi are used to encode the clock valuations in the i–th steps of the k-runs with the help of the variables from T , which record the time delays between the consecutive actions.
Recall that P = {p1, p2, . . . , pm} is a set of the parameters ranging over N. With a slight notational abuse we treat P as a set of the variables of real sort. In the current version, SMT-lib standard does not allow for typecasts between reals and integers, therefore we need to use the predicate is int to ensure that the variables from P hold integer values only (e.g., is int(7.0) evaluates to true, while is int(4.3) is false).
Summarizing, when considering the k-runs, we declare V arsk = Sik=1 Xi ∪ T ∪ P to be real variables and Bvarsk = Sik=1 BVi to be boolean variables. Additionally, we define the formula
T ypeCutk =
^ v∈V arsk v ≥ 0 ∧ ^ is int(p) p∈P which ensures that all used variables range over the appropriate sets. 3.2
In what follows, if η is a formula containing the free variables a1, a2, . . . , an, then by η[a1 ← a01, a2 ← a02, . . . an ← a0n] we denote the formula obtained by substituting a01 for a1, a02 for a2, etc. in η. Additionally, we assume that there are no two transitions having the same label in A. This assumption is not essential for the translation2, and it is used only to simplify the presentation of the results and the associated proofs.
Let tr = l act,g,r l0 be a transition, where l, l0 are respectively the source and → the target location, act is the action label, g is the guard, and r is the reset. It is convenient to use the following notations: source(tr) = l, target(tr) = l0, guard(tr) = g, and reset(tr) = r. Now, let i ∈ N. We define guardi(tr) = guard(tr)[x1 ← xi1, . . . , xn ← xin], i.e., the encoding of guard(tr) using the variables introduced earlier. Define reseti(tr) as the smallest set such that xij := a + ti ∈ reseti(tr) if xj := a ∈ reset(tr) and xij := xi−1 + ti ∈ reseti(tr) j otherwise, for each 1 ≤ j ≤ n. Intuitively, reseti(tr) models the new value of each clock after the consecutive reset and delay. Let s ∈ Q be a location, we define invi(s) = I(s)[x1 ← xi1, . . . , xn ← xin], i.e., the encoding of the invariant of s. The above notions are combined to define the encoding of the transition tr as follows: tr enci(tr) = loc enci(source(tr)) ∧ guardi(tr) ∧ reseti+1(tr)
∧ invi+1(target(tr)) ∧ loc enci+1(target(tr)).
The correctness of the above construction is stated in the following lemma. Lemma 1. Let tr = l act,g,r l0 be a transition in A, υ be a parameter valuation, → (l, ω) be a concrete state in JAKυ and i ∈ N. Then, (l, ω) −a→ct d (sla0t,iωsf[yri]n+g Vd)|=intrJAenKυci(itffr)f∧orTsyopmeCe uvtai+lu1atwioenhaVveotfhaatl:l the variabl(els0, ωin[r]V) a−r→sk – υ = V|P , – ω = V|Xi [xi1 ← x1, . . . , xin ← xn], – d = V (ti+1), – ω[r] + d = V|Xi+1 [xi1+1 ← x1, . . . , xin+1 ← xn].
Proof. Observe that the locations are uniquely represented by their encodings, thus we can focus on nonboolean variables only.
(⇐) Let V be a valuation of the variables such that V |= tr enci(tr) ∧ T ypeCuti+1. Let ω = V|Xi [xi1 ← x1, . . . , xin ← xn] and υ = V|P . Denote ωi = V|Xi , then from V |= guardi(tr) we obtain ωi |=υ guardi(tr), which in turn yields that ω |=υ guard(tr). Let d = V (ti+1), denote ωi+1 = V|Xi+1 and notice that from V |= reseti+1(tr) it follows that ωi+1(xij+1) = ωi[r](xij ) + d for all 1 ≤ j ≤ n. Thus, if we denote ω0 = V|Xi+1 [xi1+1 ← x1, . . . , xin+1 ← xn], then ω0 = ω[r] + d. Now, observe that from V |= invi+1(target(tr)) we can infer that ωi+1 |=υ invi+1(target(tr)), from which ω0 |=υ I(target(tr)), i.e., ω[r] + d |=υ I(target(tr)). As d ≥ 0 and in the view of the assumption that the invariants admit only upper bounds on clocks, we have also that ω[r] |=υ I(target(tr)). This, together with the fact that V |= T ypeCuti+1 assures that the used variables range over the correct sets, concludes this part of the proof.
(⇒) The implication in the other direction follows easily from the basic definitions of the transitions in JAυK. 2 We can always relabel the labels.
Our aim is to encode all the k-runs of Aυ for each parameter valuation υ. Recall that n is the number of the clocks. To this end we define the following formula: model enck(A) = T ypeCutk ∧
Vin=1(xi0 = t0) ∧ loc enc0(l0) ∧ inv0(l0) ∧ Vik=−01 Wtr∈ → tr enci(tr).
The first component ensures that all variables range over the proper values. The second component sets all the initial clocks to some arbitrary common value (the assumption that the invariants represent the upper bounds on the clocks is significant here), encodes the initial state, and makes sure that its invariant is satisfied. The last component encodes all the possible transitions in the k–runs.
Let φ be a state formula and i ∈ N. Let {l1, . . . , lm} be a set of all the locations present in φ. We define the encoding of φ as follows: pr enci(φ) = φ[x1 ← xi1, . . . , xn ← xin, l1 ← loc enci(l1), . . . , lm ← loc enci(lm)], i.e., we simply substitute in φ each clock with its i–th variable counterpart, and each location with its encoding using boolean variables from BVi.
We obtain the formula to be used for testing and parameter synthesis by combining the encodings of the k-runs and the property, as presented in the following lemma.
Lemma 2. Let A be a parametric timed automaton, φ be a state formula, υ be a valuation of the parameters, and k ∈ N. A state satisfying φ is k–reachable in JAKυ iff there exists a valuation V of all the variables in V arsk such that V |= model enck(A) ∧ pr enck(φ) and V|P = υ.
Proof. Due to the presence of T ypeCutk in model enck(A) we know that all the variables range over the proper sets.
Let l be the (unique) location such that V|BVk |= loc enck(l) and ωk = V|Xk [x1k ← x1, . . . , xkn ← xn], First, we prove that V |= model enck(A) iff the state (l, ωk) is k–reachable in JAυK for υ = V|P .
If k = 0, then Vin=1(xi0 = t0) ∧ loc enc0(l0) ∧ inv0(l0) is satisfied by the valuation V iff V is such that if we denote ω0 = V|X0 [x01 ← x1, . . . , x0n ← xn] and V|P = υ, then for some t0 = V (t0) we have that ω0 = ω0+t0 and ω0 |=υ I(l0). This corresponds to the set of states to which JAυK can progress by the time transitions
For the inductive step observe that model enck(A) = model enck−1(A) ∧ Wtr∈ → tr enck−1(tr)∧T ypeCutk = Wtr∈ → model enck−1(A)∧tr enck−1(tr) ∧ T ypeCutk and apply Lemma 1 and the inductive assumption.
To conclude, notice that pr enck(φ) simply encodes all the concrete states for which φ holds, using the variables from BVk ∪ Xk.
We already know how to write, for a given parametric timed automaton and a property, the formula encoding k–reachable states for which the property holds together with the associated valuations of the parameters. It might be beneficial to verify this formula as it is, if we wish to obtain the answer to the question whether the property is satisfied by k–reachable states. We can also rely on the SMT-solver to obtain an exemplary witness, i.e., a correct valuation of the parameters. Our task is, however, to systematically explore the space of the admissible parameters, with a hope for painting a part of the picture from which an analyst can make further generalizations.
Let A = hQ, l0, A, X, P, →, Ii be an L/U automaton and P = L ∪ U , where L and U are disjoint sets of the upper and the lower parameters, respectively. Assume that L = {λ1, . . . , λl} and U = {μ1, . . . , μu}.
Let φ be a property and υ be such a valuation of the parameters that there exists a reachable state in JAKυ satisfying φ. Recall (Proposition 1) that in the class of the L/U automata this means that a state satisfying φ is also reachable in JAKυ0 for each υ0 such that υ ≤ υ0.
Define the complementing clause with respect to υ as follows
ComplClause(υ) = l u _ (λi > υ(λi)) ∨ _ (μi < υ(μi)), i=1 i=1 and observe that υ0 |= ComplClause(υ) iff υ ≤ υ0 is not true.
We employ ComplClause(υ) to block the SMT-solver from seeking for parameter valuations which can be inferred from the L/U automata properties and the set of the parameters that has been already synthesized.
The following algorithm attemps to synthesise parameter valuations for which there exists a k–reachable state satisfying the property φ. If the search is successful, the user is presented with a newly synthesised parameter valuation υ and asked whether the procedure should be continued. If so, a new blocking ComplClause(υ) is added to the main formula and the loop takes another turn. Algorithm 1 ReachSynth(A, φ, k) Input: an L/U automaton A, a property φ, a depth value k ∈ N Output: a set Res of valuations of the parameters 1: Res := ∅ 2: reachF ormula := model enck(A) ∧ pr enck(φ) 3: while user requests to expand Res and reachFormula is satisfiable do 4: let V be such that V |= reachF ormula and υ := V|P 5: let Res := Res ∪ {υ} 6: let reachF ormula := reachF ormula ∧ ComplClause(υ) 7: end while 8: return Res
Note that in the above algorithm the testing for satisfiability (line 3), and extraction of the witness valuation υ of the parameters (line 4) is performed by means of a call to an external SMT-solver.
Lemma 3. Let A be an L/U automaton, φ be a property, and k ∈ N. For each valuation of the parameters υ0 such that there exists υ ∈ ReachSynth(A, φ, k) satisfying υ ≤ υ0 we have that JAKυ0 |= EF φ.
Proof. It follows immediately from Lemma 2 combined with the properties of ComplClause(υ).
The ReachSynth algorithm can be used as the main building block of a bounded
parametric model checking process. The input consists of an L/U automaton A
and a property φ. Initially, we can employ the results from [
In this section we present some preliminary results on parametric analysis of
two selected models, namely Fischer’s Mutual Exclusion Protocol and a version
of Generic Timed Pipeline Paradigm [
Definition 5. Let U = {Ai = hQi, l0i, Ai, Xi, P i, →i, Iii | 1 ≤ i ≤ m} be a set (a network) of parametric timed automata such that Xi ∩ Xj = ∅ for each 1 ≤ i, j ≤ m and i 6= j. Let L(a) = {1 ≤ i ≤ m | a ∈ Ai} be a function associating with each action a ∈ S1≤i≤m Ai the indices of the automata recognizing a. We define the product automaton A = hQ, l0, A, X, P, →, Ii of the network U , where: – Q = Qm
i=1 Qi, – l0 = (l01, . . . , l0m), – A = Sm
i=1 Ai, –– PX == SSimim==11 PXii,, – I((l1, . . . , lm)) = Vim=1 Ii(li) for each (l1, . . . , lm) ∈ Q, and the transition relation → is such that: – (l1, . . . , lm) a→,g,r (l10, . . . , lm0) iff for each i ∈ L(a) we have li a,→gi,iri li0, and g = Vi∈L(a) gi, r = Si∈L(a) ri, and li = li0 for all i ∈ {1, . . . , m} \ L(a). In addition to a network, the user is expected to supply an experiment’s plan file. Such a plan consists of a sequence of pairs (k, No) of natural numbers, where k is the length of the runs to be considered, and No is a maximal number of parameter valuations to be synthesised should the verified property be found satisfiable. Our tool goes through the pairs in accordance with increasing k, incrementally building the formulae to be tested as it was presented in earlier sections.
All the experiments have been performed on Intel P6200 2.13GHz dual core machine with 3GB memory, running Linux operating system. 5.1
The timed automata network presented in Figure 1 models one of the possible solutions to the classical problem of mutual exclusion, i.e., ensuring that only one of the competing processes is able to gain an access to the critical section.
The system in question consists of n independent processes synchronised via the shared variable X. The model contains two parameters, i.e., the lower bound parameter δ and the upper bound parameter Δ. It is well known that no two processes are able to simultaneously get to their critical sections iff Δ ≤ δ, thus we have chosen to verify the reachability of φ1 = critical1 ∧ critical2. Intuitively, this means that we aim to synthesise values of the parameters δ and Δ under which the system behaves incorrectly, allowing two competing processes to jointly enter their critical sections.
idle1 trying1 idle2
trying2
As it turns out, for each test with the positive outcome, the set of the returned valuations consists of the pairs (δ = i, Δ = i + 1) for i from 0 to the limit No = 10 given in the experiment’s plan. Clearly, from the point of view of an analyst and in light of Lemma 3 this result indeed justifies an educated guess that the mutual exclusion property is violated if Δ > δ. n k SAT? param vals max. form. form. bdg. total CVC3 peak CVC3
(Y/N) found size (MB) time (sec.) time (sec.) mem. (MB) bility, 4–th column: the number of the synthesised parameter valuations, 5–th column: the maximal (if k is an interval) size of the generated SMT-lib v2 formula, 6–th column: the time spent on incrementally building the formulae, 7–th column: the total time spent on verifying the formulae, 8–th column: the maximal memory used by CVC3 solver.
ProdReset x1 ≥ a x1 := 0 ConsReset x4 ≥ a x4 := 0
Producer prodReady x1 ≤ d prodWaiting x1 ≤ b consReady x4 ≤ d consWaiting x4 ≤ b Consumer
Feed2 x1 ≥ c x1 := 0
Feed2 x2 ≥ c x2 := 0 Feed4 x4 ≥ c x4 := 0 xx22 :≥=e0
Node1Process2 intermediate 3 x2 ≤ f node1Ready
x2 ≤ d The network presented in Figure 2 models the system consisting of the Producer feeding the Consumer with data sent through a sequence of nodes with additional processing capabilities.
The model is scalable with respect to the number n of the processing nodes and the length m of each processing node and it contains three lower (a, c, e) and three upper (b, d, f) parameters. 10 for all k.
We have decided to add one dummy clock, called xtotal, to the above system. It is straightforward to see that such an alteration does not change the behaviour of the model, and that xtotal can be used to measure the total time passed along a given run. With the help of the new clock we have analysed the reachability of φ2 = ConsW aiting ∧ P rodReady ∧ xtotal ≥ 5. Again, the limit No is set to n m k SAT? param vals max. form. form. bdg. total CVC3 peak CVC3
(Y/N) found size (MB) time (sec.) time (sec.) mem. (MB)
Note that the generated SMT formulae are rather small in this case. This
probably reflects the power of a concise representation by means of SMT
instances rather than the size of model’s state space [
We have proposed a simple translation for a direct representation of finite runs of a parametric timed automaton in form of SMT instances. This translation coupled with blocking clauses allowed us for an underapproximation of the set of the parameter valuations under which the given reachability property holds in L/U automata. To the best of our knowledge this is the first such application of SMT solvers, and this is at the same time a proof-of-concept as well as a practical tool for exploring the spaces of parameter valuations.
In the future we plan to extend our work to the parametric verification of properties more complex than reachability, e.g., the existential fragment of CTL*. Additionally, we plan to investigate the possibilites of an automated inference of more general (or even complete) constraints under which the given property holds using partial knowledge on the space of the parameter valuations obtained using the methods presented in this paper.