Verified Certification of Reachability Checking for Timed Automata
427
The idea of extracting certificates from the model checking process has
previously been studied in the context of the μ-calculus [23] and finite state
LTL model checking [27]. However, these works are not accompanied by a
verified certificate checker and do not attempt to scale the approach to practical
examples. Only the recent work of Griggio et al. [11] provides a practical extraction
mechanism and a certificate checker for LTL model checking, but the checker is
not verified. To the best of our knowledge, we are the first to examine certification
in the context of timed automata model checking.
Finally, in the context of software verification, the idea of producing certificates
for the correctness of a program has been broadly studied [16,5].
Isabelle/HOL Isabelle/HOL [25] is an interactive theorem prover based on HigherOrder Logic (HOL). HOL can be thought of as a combination of a functional
programming language and mathematical logic. Isabelle/HOL mostly resembles
standard mathematical notation. Some conventions that are borrowed from
functional programming need to be explained, however. Functions are mostly
curried, i.e. of type τ 1 ⇒ τ 2 ⇒ τ instead of τ 1 × τ 2 ⇒ τ . As a consequence,
function application is usually denoted as f a b instead of f (a, b). Function
abstraction with lambda terms uses the standard syntax λx. t (the function that
maps x to t) and can also have paired arguments λ(x, y). t. Type variables are
written
a,
b, etc. Compound types are written in postfix syntax: τ set is the
type of sets of elements of type τ . We use the Isabelle/HOL convention that
free variables are implicitly all-quantified throughout the paper. In parts of the
paper, formulas or syntax have been simplified for readability, but we have stayed
largely faithful to the Isabelle/HOL formalization.
Contributions In short, these are the main contributions of our work:
– To the best of our knowledge, we are the first to study certification of the
model checking results of reachability checking for timed automata, including
techniques to compress certificates.
– We construct a verified implementation of such a certificate checker, including
a number of optimization techniques to make it practically usable.
Outline The remainder of the paper is organized as follows. The first section
briefly recalls the theory of timed automata, and sketches the state-of-the-art
model checking process. The second section details our approach to certification
and explains how, starting from an abstract theory, a concrete verified implementation of the certificate checker can be obtained. Section three illustrates a
number of techniques to improve the certificate checker’s performance, while only
mildly increasing the formalization effort. Section four discusses two methods for
certificate compression. The paper is concluded by an experimental evaluation
and remarks on potential future work.
427
The idea of extracting certificates from the model checking process has
previously been studied in the context of the μ-calculus [23] and finite state
LTL model checking [27]. However, these works are not accompanied by a
verified certificate checker and do not attempt to scale the approach to practical
examples. Only the recent work of Griggio et al. [11] provides a practical extraction
mechanism and a certificate checker for LTL model checking, but the checker is
not verified. To the best of our knowledge, we are the first to examine certification
in the context of timed automata model checking.
Finally, in the context of software verification, the idea of producing certificates
for the correctness of a program has been broadly studied [16,5].
Isabelle/HOL Isabelle/HOL [25] is an interactive theorem prover based on HigherOrder Logic (HOL). HOL can be thought of as a combination of a functional
programming language and mathematical logic. Isabelle/HOL mostly resembles
standard mathematical notation. Some conventions that are borrowed from
functional programming need to be explained, however. Functions are mostly
curried, i.e. of type τ 1 ⇒ τ 2 ⇒ τ instead of τ 1 × τ 2 ⇒ τ . As a consequence,
function application is usually denoted as f a b instead of f (a, b). Function
abstraction with lambda terms uses the standard syntax λx. t (the function that
maps x to t) and can also have paired arguments λ(x, y). t. Type variables are
written
a,
b, etc. Compound types are written in postfix syntax: τ set is the
type of sets of elements of type τ . We use the Isabelle/HOL convention that
free variables are implicitly all-quantified throughout the paper. In parts of the
paper, formulas or syntax have been simplified for readability, but we have stayed
largely faithful to the Isabelle/HOL formalization.
Contributions In short, these are the main contributions of our work:
– To the best of our knowledge, we are the first to study certification of the
model checking results of reachability checking for timed automata, including
techniques to compress certificates.
– We construct a verified implementation of such a certificate checker, including
a number of optimization techniques to make it practically usable.
Outline The remainder of the paper is organized as follows. The first section
briefly recalls the theory of timed automata, and sketches the state-of-the-art
model checking process. The second section details our approach to certification
and explains how, starting from an abstract theory, a concrete verified implementation of the certificate checker can be obtained. Section three illustrates a
number of techniques to improve the certificate checker’s performance, while only
mildly increasing the formalization effort. Section four discusses two methods for
certificate compression. The paper is concluded by an experimental evaluation
and remarks on potential future work.