Verified Certification of Reachability Checking
for Timed Automata
Simon Wimmer and Joshua von Mutius
Fakult¨ at f¨ ur Informatik,
Technische Universit¨ at M¨ unchen,
Munich, Germany
wimmers@in.tum.de
joshua.von-mutius@tum.de
Abstract. Prior research has shown how to construct a mechanically
verified model checker for timed automata, a popular formalism for
modeling real-time systems.
In this paper, we shift the focus from verified model checking to certifying unreachability. This allows us to benefit from better approximation
operations for symbolic states, and reduces execution time by exploring
fewer states and by exploiting parallelism. Moreover, this gives us the
ability to audit results of unverified model checkers that implement a
range of further optimizations, including certificate compression.
The resulting tool is evaluated on a set of standard benchmarks to
demonstrate its practicality, using a new unverified model checker implementation in Standard ML to construct the certificates.
Keywords: Timed automata · Certification · Model Checking · Interactive Theorem Proving · Isabelle/HOL
Timed automata [1] are a widely used formalism for modeling real-time systems,
which is employed in a class of successful model checkers such as Uppaal [4].
These tools can be understood as trust-multipliers: we trust their correctness to
deduce trust in the safety of systems checked by these tools. As a consequence,
one wants to ensure as rigorously as possible that the computation results of
timed automata model checkers are correct.
Previous work [31] has addressed this problem by constructing a model checker
for timed automata that is fully verified using Isabelle/HOL [25]. This tool is
intended to be a reference implementation that can be used to scrutinize the
correctness of other model checkers. As such, it is mainly able to check small
and medium-sized benchmark examples, but the performance gap w.r.t. more
practical model checkers prevents it from checking realistic benchmark models
within reasonable time and space bounds.
We address this issue by shifting the focus from full verified model checking to
only certifying that the result produced by an unverified model checker is correct.
We only study reachability: it is the most important property that is checked
with timed automata model checkers, and some model checkers only support
reachability. It is crucial to ensure that a bad state is certainly not reachable if
c
The Author(s) 2020
A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12078, pp. 425–443, 2020.
https://doi.org/10.1007/978-3-030-45190-5 24
TACAS
Evaluation
Artifact
2020
Accepted
for Timed Automata
Simon Wimmer and Joshua von Mutius
Fakult¨ at f¨ ur Informatik,
Technische Universit¨ at M¨ unchen,
Munich, Germany
wimmers@in.tum.de
joshua.von-mutius@tum.de
Abstract. Prior research has shown how to construct a mechanically
verified model checker for timed automata, a popular formalism for
modeling real-time systems.
In this paper, we shift the focus from verified model checking to certifying unreachability. This allows us to benefit from better approximation
operations for symbolic states, and reduces execution time by exploring
fewer states and by exploiting parallelism. Moreover, this gives us the
ability to audit results of unverified model checkers that implement a
range of further optimizations, including certificate compression.
The resulting tool is evaluated on a set of standard benchmarks to
demonstrate its practicality, using a new unverified model checker implementation in Standard ML to construct the certificates.
Keywords: Timed automata · Certification · Model Checking · Interactive Theorem Proving · Isabelle/HOL
Timed automata [1] are a widely used formalism for modeling real-time systems,
which is employed in a class of successful model checkers such as Uppaal [4].
These tools can be understood as trust-multipliers: we trust their correctness to
deduce trust in the safety of systems checked by these tools. As a consequence,
one wants to ensure as rigorously as possible that the computation results of
timed automata model checkers are correct.
Previous work [31] has addressed this problem by constructing a model checker
for timed automata that is fully verified using Isabelle/HOL [25]. This tool is
intended to be a reference implementation that can be used to scrutinize the
correctness of other model checkers. As such, it is mainly able to check small
and medium-sized benchmark examples, but the performance gap w.r.t. more
practical model checkers prevents it from checking realistic benchmark models
within reasonable time and space bounds.
We address this issue by shifting the focus from full verified model checking to
only certifying that the result produced by an unverified model checker is correct.
We only study reachability: it is the most important property that is checked
with timed automata model checkers, and some model checkers only support
reachability. It is crucial to ensure that a bad state is certainly not reachable if
c
The Author(s) 2020
A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12078, pp. 425–443, 2020.
https://doi.org/10.1007/978-3-030-45190-5 24
TACAS
Evaluation
Artifact
2020
Accepted