@InCollection{	  basin.ea:verification:2005,
  abstract	= {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 di erent 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.},
  author	= {David Basin and Hironobu Kuruma and Kazuo Takaragi and
		  Burkhart Wolff },
  booktitle	= {Formal Methods 2005},
  language	= {USenglish},
  pages		= {269--285},
  pdf		= {papers/2005/2_fm.pdf},
  publisher	= {Springer Verlag},
  series	= {LNCS 3582},
  title		= {Verification of a Signature Architecture with HOL-Z},
  year		= 2005,
  user		= {basin}
}