Français Anglais
Accueil Annuaire Plan du site
Home > Research results > Research highlights
Research results
Research highlight : VERIFYING A SIGNATURE ARCHITECTURE: A COMPARATIVE CASE STUDY.
VERIFYING A SIGNATURE ARCHITECTURE: A COMPARATIVE CASE STUDY.
8 October 2007

David Basin and Hironobu Kuruma and Kunihiko Miyazaki and Kazuo Takaragi and Burkhart Wolff. Verifying a signature architecture: a comparative case study. In Formal Aspects of Computing, 19 (1), pages 63-91, 2007.
We report on a case study in applying different formal methods to model and verify an architecture for administrating digital signatures. The architecture comprises several concurrently executing systems that authenticate users and generate and store digital signatures by passing security relevant data through a tightly controlled interface. The architecture is interesting from a formal-methods perspective as it involves complex operations on data as well as process coordination and hence is a candidate for both data-oriented and process-oriented formal methods.We have built and verified two models of the signature architecture using two representative formal methods. In the first, we specify a data model of the architecture in Z that we extend to a trace model and interactively verify by theorem proving. In the second, we model the architecture as a system of communicating processes that we verify by finite-state model checking. 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 complex operations on data. Moreover, our comparison highlights the advantages of proving theorems about such models and provides evidence that, in the hands of an experienced user, theorem proving may be neither substantially more time-consuming nor more complex than model checking.



Keyword
  [none]

Group
  [none]

Contact
  ° WOLFF Burkhart
Research highlights
MODEL TRANSFORMATION AS CONSERVATIVE THEORY-TRANSFORMATION
30 October 2020
We present a new technique to construct tool support for domain-specific languages (DSLs) inside the

BEST STUDENT PAPER AWARD (ML) AT ECML 2019
20 September 2019
Guillaume Doquet (A&O) received the Best Student Paper Award (category Machine Learning) at ECML 201

BEST PAPER AWARD - HPCS 2019 - ON SERVER-SIDE FILE ACCESS PATTERN MATCHING
17 July 2019
Francieli Zanon Boito¹ , Ramon Nou², Laércio Lima Pilla³, Jean Luca Bez⁴, Jean-François Méhaut¹, T

BEST FULL PAPER AWARD EDM 2019 - EDUCATIONAL DATA MINING
5 July 2019
DAS3H: Modeling Student Learning and Forgetting for Optimally Scheduling Distributed Practice of Ski

BEST PAPER AWARD - CODIT2019 - STOCHASTIC DUAL DYNAMIC INTEGER PROGRAMMING FOR A MULTI-ECHELON LOT-SIZING PROBLEM WITH REMANUFACTURING AND LOST SALES
14 May 2019
Franco Quezada, Céline Gicquel and Safia Kedad-Sidhoum