Guidelines for Formal Domain Modeling in Event-B

Atif Mashkoor 1 Jean-Pierre Jacquot 1
1 DEDALE - Development of specifications
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Abstract--In this paper, we explore the possibility to use Event-B as a formal domain modeling tool. We identify the areas where domain modelers can struggle and present some guidelines to avoid these pitfalls. We mainly address three questions about domain modeling: what to specify, how to refine, and how to verify. We discuss the strategy to express domain assumptions, protocols, time, and temporal properties. We also analyze the refinement and proof system of Event-B in this realm. We advocate small incremental steps and alternative refinement mechanisms, such as "observation levels." We find animation a very helpful activity to complement the verification process.
Type de document :
Communication dans un congrès
The 13th IEEE International High Assurance Systems Engineering Symposium (HASE 2011), Nov 2011, Boca Raton, United States. 2011
Liste complète des métadonnées

Littérature citée [29 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00640203
Contributeur : Atif Mashkoor <>
Soumis le : jeudi 10 novembre 2011 - 22:15:23
Dernière modification le : mardi 24 avril 2018 - 13:36:20
Document(s) archivé(s) le : jeudi 15 novembre 2012 - 11:45:17

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00640203, version 1

Collections

Citation

Atif Mashkoor, Jean-Pierre Jacquot. Guidelines for Formal Domain Modeling in Event-B. The 13th IEEE International High Assurance Systems Engineering Symposium (HASE 2011), Nov 2011, Boca Raton, United States. 2011. 〈hal-00640203〉

Partager

Métriques

Consultations de la notice

181

Téléchargements de fichiers

354