Verified Certification of Reachability Checking for Timed Automata
435
In the formalization, these proofs rely on instantiating a general theory of
simulations in transition systems that is derived from the theory of Wimmer and
Lammich [31]. From Corollary 1 we get that there is no reachable final state in
→ ZG(A) if the certificate check is passed. Finally, by correctness of the renaming
process and the product construction, we can conclude that there is no final
reachable state in the input model if there is no final reachable state in → A .
2.4 Implementing a Concrete Checker
All the elementary model checking primitives we need for certification have
already been implemented [31]. The abstract implementation presented above
assumes that the model checking primitives are implemented in a purely functional
manner (as they are just regular HOL functions). The existing (verified) model
checker [31], however, is an imperative implementation in the Imperative HOL
framework. Imperative HOL [7] is a framework for specifying and reasoning about
imperative programs in Isabelle/HOL. It provides a heap monad in which one
can use—analogously to the ML family of programming languages—imperative
references and arrays to express imperative programs. Usually, once we have used
an imperative implementation anywhere, the whole program would need to be
stated in the heap monad. However, we can employ a technique similar to the
one that is used for Haskell’s ST monad [21] to erase the heap monad in a safe
way under certain circumstances.
More precisely, if it can be deduced from the type of an imperative computation
that no information about references or arrays on the heap can be leaked to the
outside of the computation in its result, then the heap monad can be erased for
this computation, yielding a pure computation. In the certifier, this is primarily
used for computing the symbolic successor of a zone Z for a certain transition.
To that end, an immutable representation of the DBM M corresponding to Z is
copied to the a newly allocated imperative array, then the imperative pipeline
of computations to compute the successor M
is applied to M , and finally M
is copied back to an immutable array. Taken together, this whole computation
does not contain the type of an array or reference in its result type, and thus
can safely be turned into a pure computation. As a consequence, we are able to
reuse the existing verified model checking primitives, while being able to state
the certificate checking algorithm purely functionally.
In the concrete checker, the mapping M is implemented using a verified
functional hash table implementation based on so-called diff arrays [19]. This
data structure provides a purely functional interface to an underlying imperative
array. When a diff array is updated, it performs the update on the imperative
array, and stores a difference that can be used to re-compute the old state of the
array. Reading from the most recent version of a diff array is fast as the value
can directly be read from the underlying imperative array. If an old version is
accessed, the whole array has to be copied to recompute the old version. This
gives diff arrays good performance characteristics, as long as they are mostly
used linearly. This is the case in our application as the hash table is filled in an
initial phase, after which the hash table is used in a read-only manner.
435
In the formalization, these proofs rely on instantiating a general theory of
simulations in transition systems that is derived from the theory of Wimmer and
Lammich [31]. From Corollary 1 we get that there is no reachable final state in
→ ZG(A) if the certificate check is passed. Finally, by correctness of the renaming
process and the product construction, we can conclude that there is no final
reachable state in the input model if there is no final reachable state in → A .
2.4 Implementing a Concrete Checker
All the elementary model checking primitives we need for certification have
already been implemented [31]. The abstract implementation presented above
assumes that the model checking primitives are implemented in a purely functional
manner (as they are just regular HOL functions). The existing (verified) model
checker [31], however, is an imperative implementation in the Imperative HOL
framework. Imperative HOL [7] is a framework for specifying and reasoning about
imperative programs in Isabelle/HOL. It provides a heap monad in which one
can use—analogously to the ML family of programming languages—imperative
references and arrays to express imperative programs. Usually, once we have used
an imperative implementation anywhere, the whole program would need to be
stated in the heap monad. However, we can employ a technique similar to the
one that is used for Haskell’s ST monad [21] to erase the heap monad in a safe
way under certain circumstances.
More precisely, if it can be deduced from the type of an imperative computation
that no information about references or arrays on the heap can be leaked to the
outside of the computation in its result, then the heap monad can be erased for
this computation, yielding a pure computation. In the certifier, this is primarily
used for computing the symbolic successor of a zone Z for a certain transition.
To that end, an immutable representation of the DBM M corresponding to Z is
copied to the a newly allocated imperative array, then the imperative pipeline
of computations to compute the successor M
is applied to M , and finally M
is copied back to an immutable array. Taken together, this whole computation
does not contain the type of an array or reference in its result type, and thus
can safely be turned into a pure computation. As a consequence, we are able to
reuse the existing verified model checking primitives, while being able to state
the certificate checking algorithm purely functionally.
In the concrete checker, the mapping M is implemented using a verified
functional hash table implementation based on so-called diff arrays [19]. This
data structure provides a purely functional interface to an underlying imperative
array. When a diff array is updated, it performs the update on the imperative
array, and stores a difference that can be used to re-compute the old state of the
array. Reading from the most recent version of a diff array is fast as the value
can directly be read from the underlying imperative array. If an old version is
accessed, the whole array has to be copied to recompute the old version. This
gives diff arrays good performance characteristics, as long as they are mostly
used linearly. This is the case in our application as the hash table is filled in an
initial phase, after which the hash table is used in a read-only manner.