438
S. Wimmer and J. von Mutius
c) the convex hull of the first two zones that can successfully be joined is put to
the front of the list;
d) same as c) but considering only discrete states for which compression was
successful in the last round;
e) same as d) but iterating the operation until saturation.
The next section contains an experimental evaluation of these techniques.
Note that similar techniques for reducing the search-space could also be applied
already during model checking. By doing so, the number of states explored and
the runtime of model checking could be reduced. This, however, comes at the
risk of producing spurious model checking results (i.e. a final state might be
deemed reachable, although there is no corresponding reachable state in the
timed automaton).
5 Experimental Evaluation
We evaluate the checker on a set of benchmarks that is derived from Uppaal’s
standard benchmark suite [22]. Additionally, to cover the advanced modeling
features of committed locations and broadcast channels, we use a set of benchmarks that is derived from the pacemaker models of Jiang et al. [17] and a
modified version of the FDDI benchmark with broadcast channels. A prototype
SML implementation of a timed automata model checker (Mlunta) is used to
compute the certificates. We use reachability properties of the form E♦ false to
enforce that the model checker explores the complete state space. The results are
given in Table 1. The problem size is specified as the number of automata in the
network. We report the total runtime (wall time) of:
1. the tandem consisting of Mlunta (using the first compression technique) and
the (verified) certificate checker, both compiled with MLton;
2. the individual runtime of the (verified) certificate checker for a varying number
of threads for parallel computation, compiled with Poly/ML as it is the only
SML compiler that supports multi-threading;
3. the runtime of Uppaal configured for depth-first search (like Mlunta);
4. the runtime of an unverified SML implementation of the certificate checker
based on Mlunta (compiled with MLton);
5. and the runtime of the fully verified model checker Munta [31] extended with
the improvements from sections 2 and 4 and compiled with MLton.
As can be seen from the results, the tandem is still one order of magnitude
slower than Uppaal, but certificate checking in isolation is also up to one order of
magnitude faster than the previous verified model checker [31]. Note that Mlunta
explores significantly more states than Uppaal and Munta for “Pacemaker”.
Multi-core scale beyond two threads is relatively unsatisfactory, however. In microbenchmarks, we have identified that the problem appears to be with memory
allocation on the heap, even if no data is shared among threads (in our case, only
the certificate is shared but successors are computed locally). There does not
S. Wimmer and J. von Mutius
c) the convex hull of the first two zones that can successfully be joined is put to
the front of the list;
d) same as c) but considering only discrete states for which compression was
successful in the last round;
e) same as d) but iterating the operation until saturation.
The next section contains an experimental evaluation of these techniques.
Note that similar techniques for reducing the search-space could also be applied
already during model checking. By doing so, the number of states explored and
the runtime of model checking could be reduced. This, however, comes at the
risk of producing spurious model checking results (i.e. a final state might be
deemed reachable, although there is no corresponding reachable state in the
timed automaton).
5 Experimental Evaluation
We evaluate the checker on a set of benchmarks that is derived from Uppaal’s
standard benchmark suite [22]. Additionally, to cover the advanced modeling
features of committed locations and broadcast channels, we use a set of benchmarks that is derived from the pacemaker models of Jiang et al. [17] and a
modified version of the FDDI benchmark with broadcast channels. A prototype
SML implementation of a timed automata model checker (Mlunta) is used to
compute the certificates. We use reachability properties of the form E♦ false to
enforce that the model checker explores the complete state space. The results are
given in Table 1. The problem size is specified as the number of automata in the
network. We report the total runtime (wall time) of:
1. the tandem consisting of Mlunta (using the first compression technique) and
the (verified) certificate checker, both compiled with MLton;
2. the individual runtime of the (verified) certificate checker for a varying number
of threads for parallel computation, compiled with Poly/ML as it is the only
SML compiler that supports multi-threading;
3. the runtime of Uppaal configured for depth-first search (like Mlunta);
4. the runtime of an unverified SML implementation of the certificate checker
based on Mlunta (compiled with MLton);
5. and the runtime of the fully verified model checker Munta [31] extended with
the improvements from sections 2 and 4 and compiled with MLton.
As can be seen from the results, the tandem is still one order of magnitude
slower than Uppaal, but certificate checking in isolation is also up to one order of
magnitude faster than the previous verified model checker [31]. Note that Mlunta
explores significantly more states than Uppaal and Munta for “Pacemaker”.
Multi-core scale beyond two threads is relatively unsatisfactory, however. In microbenchmarks, we have identified that the problem appears to be with memory
allocation on the heap, even if no data is shared among threads (in our case, only
the certificate is shared but successors are computed locally). There does not