Technical Report
Integrating Theorem Proving and Model Checking in {I}sabelle/{IOA}
Author(s): Tobias Hamberger
Year: 1999
Number: TUM-I
Editor:
CR Classification: F.3.0, G.4
CR General Terms: Theory, Verification
Keywords: Isabelle, Integration, Verification, Model Checking, Mucke, Input/Output Automata
Abstract:Isabelle is a generic theorem proving environment which was used
successfully in
recent years for many practical applications.
In particular, the model of
Input/Output-automata in combination
with its formal meta-theory, abstraction
theory and temporal logic
has been embedded in Isabelle/HOLCF. An advantage of
Isabelle is, that
it can cope with arbitrary large systems, even infinite in
the number of states.
A disadvantage is the necessary interaction of the user
during
verification process. On the other hand, model checkers enable
automatical verification, but their use is usually restricted
to small, finite
systems.
In this paper, we present an integrated environment for
specification and verification
of distributed systems in Isabelle. Beginning
with the Isabelle formulation
of I/O-automata, some additional components were
created by the author
and assembled to a consistent tool. Here, we take a
closer look
on the integration of the model checker $\mu$cke as an external
verification tool
for Isabelle.\\
We also present a direct support of the
specification language for I/O-automata
known from literature and we present a
proof tactic for
implementation relations of I/O-automata in Isabelle. The
model checker
$\mu$cke, which is used in this tactic, is integrated in Isabelle
as an oracle.
The usage of the resulting verification environment for reactive
systems
is presented by two examples.
Available as compressed Postscript
BibTeX-Entry:
<![CDATA[
@techreport{Ham-MC-99,
author = {Tobias Hamberger},
title = {Integrating Theorem Proving and Model Checking in {I}sabelle/{IOA}},
number = {TUM-I},
institution = {Technische Univerit\"at M\"unchen},
year = {1999},
url = {http://www4.informatik.tu-muenchen.de/reports/Ham-MC-99.html},
abstract = {Isabelle is a generic theorem proving environment which was used
successfully in
recent years for many practical applications.
In particular, the model of
Input/Output-automata in combination
with its formal meta-theory, abstraction
theory and temporal logic
has been embedded in Isabelle/HOLCF. An advantage of
Isabelle is, that
it can cope with arbitrary large systems, even infinite in
the number of states.
A disadvantage is the necessary interaction of the user
during
verification process. On the other hand, model checkers enable
automatical verification, but their use is usually restricted
to small, finite
systems.
In this paper, we present an integrated environment for
specification and verification
of distributed systems in Isabelle. Beginning
with the Isabelle formulation
of I/O-automata, some additional components were
created by the author
and assembled to a consistent tool. Here, we take a
closer look
on the integration of the model checker $\mu$cke as an external
verification tool
for Isabelle.\\
We also present a direct support of the
specification language for I/O-automata
known from literature and we present a
proof tactic for
implementation relations of I/O-automata in Isabelle. The
model checker
$\mu$cke, which is used in this tactic, is integrated in Isabelle
as an oracle.
The usage of the resulting verification environment for reactive
systems
is presented by two examples.},
CRClassification = {F.3.0, G.4},
CRGenTerms = {Theory, Verification}}
]]>
See also the Isabelle/IOA page