426
S. Wimmer and J. von Mutius
the model checker claims so, thus we want to certify unreachability. Certifying
that a state is indeed reachable would amount to extracting a timed trace and
certifying that the trace is compatible with the model. While implementing this
in a verified manner would be comparatively easy, we consider it less important
because it corresponds to the bug finding functionality of model checkers, which
carries less trust.
The recipe for certifying unreachability is simple: the model checker explores a
number of states until it determines that there are no more states to be found. If
none of the states fulfill the final state predicate (i.e. violates the safety property),
then the model checker will answer “unreachable”. We use the set of explored
states as the unreachability certificate. In essence, we only need to check that
the initial state is contained in this set, that there are no outgoing edges from
this set, and that none of the states in the set fulfill the final state predicate.
The switch to certification holds many advantages. Timed automata model
checking uses over-approximations of symbolic states to ensure termination. A
large variety of these approximation operators has been studied [2,3,14]. Our
previous work [29] has shown that, while formally proving the correctness of these
approximation operations is feasible in principle with an interactive theorem
prover, the effort is rather high. Instead, to certify unreachability, it is sufficient
to only know that the approximation operator indeed yields a state that is at
least as big as the precise symbolic state. Certifying this property is cheap.
Moreover, certification eases parallelization. Checking that a state is not final
and that all its successors are covered by the state set are local properties. We
show how to exploit this in a verified implementation, while only mildly increasing
the verification effort and the size of the trusted code base.
Finally, the number of states explored by a model checker can vary immensely,
depending on a range of factors such as the chosen approximation operator or
the search order. Thus, an efficient unverified tool can exploit different heuristics
and strategies to compute a state space that is as small as possible, and thereby
speedup the certification effort. In this context, we also study a number of
compression techniques to reduce the number of states in the certificate after the
model checker has concluded its search.
We use a new unverified model checker called Mlunta, which is implemented
in Standard ML (SML), to generate certificates for a set of standard benchmarks,
and to evaluate our verified certifier’s performance on these benchmarks
1 .
Related Work This work is based on an existing Isabelle/HOL formalization of
timed automata model checking [29,31]. Other proof-assistant formalizations of
timed automata focus on proving elementary properties about the basic formalism
[33,34], or proving properties about concrete automata [26,10,8], but none of
them are concerned with model checking.
Earlier work formalizes a model checker for the modal μ-calculus [28], and
constructs a verified finite state LTL model checker [9,24,6].
1 Both tools are available online: https://doi.org/10.5281/zenodo.3679245.
S. Wimmer and J. von Mutius
the model checker claims so, thus we want to certify unreachability. Certifying
that a state is indeed reachable would amount to extracting a timed trace and
certifying that the trace is compatible with the model. While implementing this
in a verified manner would be comparatively easy, we consider it less important
because it corresponds to the bug finding functionality of model checkers, which
carries less trust.
The recipe for certifying unreachability is simple: the model checker explores a
number of states until it determines that there are no more states to be found. If
none of the states fulfill the final state predicate (i.e. violates the safety property),
then the model checker will answer “unreachable”. We use the set of explored
states as the unreachability certificate. In essence, we only need to check that
the initial state is contained in this set, that there are no outgoing edges from
this set, and that none of the states in the set fulfill the final state predicate.
The switch to certification holds many advantages. Timed automata model
checking uses over-approximations of symbolic states to ensure termination. A
large variety of these approximation operators has been studied [2,3,14]. Our
previous work [29] has shown that, while formally proving the correctness of these
approximation operations is feasible in principle with an interactive theorem
prover, the effort is rather high. Instead, to certify unreachability, it is sufficient
to only know that the approximation operator indeed yields a state that is at
least as big as the precise symbolic state. Certifying this property is cheap.
Moreover, certification eases parallelization. Checking that a state is not final
and that all its successors are covered by the state set are local properties. We
show how to exploit this in a verified implementation, while only mildly increasing
the verification effort and the size of the trusted code base.
Finally, the number of states explored by a model checker can vary immensely,
depending on a range of factors such as the chosen approximation operator or
the search order. Thus, an efficient unverified tool can exploit different heuristics
and strategies to compute a state space that is as small as possible, and thereby
speedup the certification effort. In this context, we also study a number of
compression techniques to reduce the number of states in the certificate after the
model checker has concluded its search.
We use a new unverified model checker called Mlunta, which is implemented
in Standard ML (SML), to generate certificates for a set of standard benchmarks,
and to evaluate our verified certifier’s performance on these benchmarks
1 .
Related Work This work is based on an existing Isabelle/HOL formalization of
timed automata model checking [29,31]. Other proof-assistant formalizations of
timed automata focus on proving elementary properties about the basic formalism
[33,34], or proving properties about concrete automata [26,10,8], but none of
them are concerned with model checking.
Earlier work formalizes a model checker for the modal μ-calculus [28], and
constructs a verified finite state LTL model checker [9,24,6].
1 Both tools are available online: https://doi.org/10.5281/zenodo.3679245.