[isabelle] Paper available
Dear Isabelle Users,
perhaps you might be interested in the following paper,
in particular if you are interested in empirical data
over the never-ending debate "Model-Checking or Theorem Proving?".
David Basin and Hironobu Kuruma and Kazuo Takaragi and
Verification of a Signature Architecture with HOL-Z.
In Formal Methods 2005.
LNCS 3582 Springer Verlag, pp. 269--285, 2005.
Computer Security Group, ETH Zürich
We report on a case study in using HOL-Z, an embedding of Z in
higher-order logic, to specify and verify a security architecture
for administering digital signatures. We have used HOL-Z to
formalize and combine both data-oriented and process-oriented
architectural views. Afterwards, we formalized temporal requirements
in Z and carried out verification in higher-order logic. The same
architecture has been previously verified using the SPIN model
checker. Based on this, we provide a detailed comparison of these two
different approaches to formalization (infinite state with rich data
types versus finite state) and verification (theorem proving versus#
model checking). Contrary to common belief, our case study suggests
that Z is well suited for temporal reasoning about process models
with rich data. Moreover, our comparison highlights the advantages of
this approach and provides evidence that, in the hands of experienced
users, theorem proving is neither substantially more time-consuming
nor more complex than model checking.
bwolff <bwolff at inf.ethz.ch>
This archive was generated by a fusion of
Pipermail (Mailman edition) and