Safe Decomposition of Startup Requirements
167
DOMAIN :=
1≤c≤n
1≤i≤|c|
( ¯ l
c
i ≥ 0 ∧ ¯ l
c
i ≤ ¯
u
c
i )
REFINE :=
1≤c≤n
1≤i≤|c|
u
c
i =∞
(a
c
i ≤ ¯ l
c
i ∧ ¯
u
c
i ≤ b
c
i )
The symbolic representation of the feasible region R is given by:
SYNTH := DOMAIN ∧ REFINE ∧ ¬∃S, R
W ill
(10)
By removing the existential quantification on S and R (this can be done by means
of quantifier elimination techniques), we obtain a quantifier-free formula over the
variables in Π. By construction, we have that each model γ of SYNTH is a feasible valuation, and viceversa. Therefore SYNTH is the symbolic representation
of the feasible region R.
5 Experimental Evaluation
We implemented the encoding described in Sec. 3.2 in a tool called TRICker
(Timing Requirements Integration Checker)
6 , which uses MathSAT [12] as the
backend SMT engine. We compared TRICker with Uppaal [6] and Timed-nuXmv
[8], both using the automata-based encoding described in Sec. 3.1.
The test set is partitioned into three categories: (i) bounded convex contains
only systems with finite bounds and convex state dependencies; (ii) bounded
contains systems with only finite bounds, but with arbitrary dependencies (not
necessarily convex); (iii) general contains systems with infinite bounds and
arbitrary dependencies (this is the most general fragment). Each category in turn
consists of ca. 500 randomly-generated systems, divided in 10 sub-categories,
namely 2c3p, 2c15p, 5c3p, 5c20p, 10c4p, 10c30p, 50c5p, 50c30p, 100c3p
and 100c10p, where N cM p is the category containing only systems with N
components and (approximately) M phases for each component. Inside each
sub-category, each benchmark is randomly generated, meaning that the exact
number of phases for each component and the density of its signal and state
dependencies was chosen uniformly at random. For each benchmark, we compare
the time spent by the three tools on the consistency checking and compatibility
checking problems. We ran the experiments on a cluster of Linux machines with
a 2.27GHz Xeon CPU, with a timeout of 360 seconds for each instance.
We consider first the bounded convex category. Fig. 3 shows the comparison
of TRICker with Timed-nuXmv and Uppaal on the two verification problems. In
both cases, Timed-nuXmv runs the infinite-state variant of IC3 described in [11]
after discretizing the timed automata. As for Uppaal, we verify a property in
the form EF ϕ, where ϕ is a Boolean formula. For both problems, the SMTbased approach implemented in TRICker outperforms the model checkers. While
there are a number of instances for which the model checkers perform better
6 http://users.dimi.uniud.it/ ∼ luca.geatti/tricker.html
167
DOMAIN :=
1≤c≤n
1≤i≤|c|
( ¯ l
c
i ≥ 0 ∧ ¯ l
c
i ≤ ¯
u
c
i )
REFINE :=
1≤c≤n
1≤i≤|c|
u
c
i =∞
(a
c
i ≤ ¯ l
c
i ∧ ¯
u
c
i ≤ b
c
i )
The symbolic representation of the feasible region R is given by:
SYNTH := DOMAIN ∧ REFINE ∧ ¬∃S, R
W ill
(10)
By removing the existential quantification on S and R (this can be done by means
of quantifier elimination techniques), we obtain a quantifier-free formula over the
variables in Π. By construction, we have that each model γ of SYNTH is a feasible valuation, and viceversa. Therefore SYNTH is the symbolic representation
of the feasible region R.
5 Experimental Evaluation
We implemented the encoding described in Sec. 3.2 in a tool called TRICker
(Timing Requirements Integration Checker)
6 , which uses MathSAT [12] as the
backend SMT engine. We compared TRICker with Uppaal [6] and Timed-nuXmv
[8], both using the automata-based encoding described in Sec. 3.1.
The test set is partitioned into three categories: (i) bounded convex contains
only systems with finite bounds and convex state dependencies; (ii) bounded
contains systems with only finite bounds, but with arbitrary dependencies (not
necessarily convex); (iii) general contains systems with infinite bounds and
arbitrary dependencies (this is the most general fragment). Each category in turn
consists of ca. 500 randomly-generated systems, divided in 10 sub-categories,
namely 2c3p, 2c15p, 5c3p, 5c20p, 10c4p, 10c30p, 50c5p, 50c30p, 100c3p
and 100c10p, where N cM p is the category containing only systems with N
components and (approximately) M phases for each component. Inside each
sub-category, each benchmark is randomly generated, meaning that the exact
number of phases for each component and the density of its signal and state
dependencies was chosen uniformly at random. For each benchmark, we compare
the time spent by the three tools on the consistency checking and compatibility
checking problems. We ran the experiments on a cluster of Linux machines with
a 2.27GHz Xeon CPU, with a timeout of 360 seconds for each instance.
We consider first the bounded convex category. Fig. 3 shows the comparison
of TRICker with Timed-nuXmv and Uppaal on the two verification problems. In
both cases, Timed-nuXmv runs the infinite-state variant of IC3 described in [11]
after discretizing the timed automata. As for Uppaal, we verify a property in
the form EF ϕ, where ϕ is a Boolean formula. For both problems, the SMTbased approach implemented in TRICker outperforms the model checkers. While
there are a number of instances for which the model checkers perform better
6 http://users.dimi.uniud.it/ ∼ luca.geatti/tricker.html