Email Gateway (Aug 17 2022 at 13:26): Email Gateway (Aug 17 2022 at 13:26):From: bwolff <bwolff@inf.ethz.ch>
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
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
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.
URL:http://kisogawa.inf.ethz.ch/WebBIB/publications/papers/2005/3_fm.pdf
bu
Email Gateway (Aug 18 2022 at 09:42):From: Burkhart Wolff <bwolff@inf.ethz.ch>
Dear all,
we are happy to announce our paper:
D. Basin, H. Kuruma, K. Miyazaki, K. Takaragi and B. Wolff:
Verifying a Signature Architecture - A Comparative Case Study.
In Formal Aspects of Computing, 2006.
To appear.
Abstract:
http://kisogawa.inf.ethz.ch/cgi-bin/publications/extract_abstract.cgi?DATABASE=infsec&KEY=basin.ea:verifying:2006
PDF: http://kisogawa.inf.ethz.ch/WebBIB/publications/papers/2006/fac.pdf
The paper reports on a substantial case study from the field of
computer security that had been done both with a model checking
approach and a theorem proving approach, such that empirical
data could be gained over what time had be invested to what
activity in both approaches.
The case-study gives some evidence, that theorem proving
isn't that ineffective after all, in particular if both
behavioral and data-modeling aspects are non-trivial and
if the modeling problem is open at the beginning (i.e. it
is unclear how to formalize the intended properties.)
In our case, theorem proving did not use (significantly) more
time, it used more expertise. And model-checking did have
a significant risc to prove valid, but inintended properties.
Enjoy!
Best regards
Burkhart Wolff (and David Basin)
Last updated: May 03 2024 at 12:27 UTC