[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 
   Burkhart Wolff:
   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 MHonArc.