Guidelines for Formal Domain Modeling in Event-B - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2011

Guidelines for Formal Domain Modeling in Event-B

Atif Mashkoor
  • Fonction : Auteur
  • PersonId : 854132
Jean-Pierre Jacquot
  • Fonction : Auteur
  • PersonId : 830614

Résumé

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.
Fichier principal
Vignette du fichier
main.pdf (105.65 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-00640203 , version 1 (10-11-2011)

Identifiants

  • HAL Id : hal-00640203 , version 1

Citer

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. ⟨hal-00640203⟩
81 Consultations
451 Téléchargements

Partager

Gmail Facebook X LinkedIn More