Enhancing the expressivity and automation of an interactive theorem prover in order to verify multicast protocols
View/ Open
Date
11/2006Author
Ridge, Thomas
Metadata
Abstract
This thesis was motivated by a case study involving the formalisation
of arguments that simplify the verification of tree-oriented multicast
protocols. As well as covering the case study itself, it discusses
our solution to problems we encountered concerning expressivity and
automation.
The expressivity problems related to the need for theory
interpretation. We found the existing Locale and axiomatic type class
mechanisms provided by the Isabelle theorem prover we were using to be
inadequate. This led us to develop a new prototype implementation of
theory interpretation. To support this implementation, we developed a
novel system of proof terms for the HOL logic that we also describe in
this thesis.
We found existing automation to perform poorly, which led us to
experiment with additional kinds of automation. We describe our
approach, focusing on features that make automation suitable for
interactive use.
Our presentation of the case study starts with our formalisation of an
abstract theory of distributed systems, covering state transition
systems, forward and backward simulation relations, and related
properties of LTL (linear temporal logic). We then summarise proofs of
simulation relations holding for particular abstract multicast
protocols.
We discuss the mechanisation styles we experimented with in the case
study. We also discuss the methodology behind our proofs. We cover
aspects such as how to discover and construct proofs, and how to
explore the space of proofs, how to make good definitions and lemmas,
how to increase modularity, reuse, stability and malleability of
proofs, and reduce maintenance of proofs, and the gap between
intuitively understood proofs and their formalisation.