Utilizing Event-B for Domain Engineering: A Critical Analysis

Atif Mashkoor 1 Jean-Pierre Jacquot 1
1 DEDALE - Development of specifications
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : This paper presents our experience of modeling land transportation domain in the formal framework of Event-B. Well-specified requirements are crucial for good software design; they depend on the understanding of the domain. Thus, domain engineering becomes an essential activity. The possibility to have a formal model of a domain, consistent with the use of formal methods for developing critical software working within it, is an important issue. Safety-critical domains, like transportation, exhibit interesting features, such as high levels of non-determinism, complex interactions, stringent safety properties, multifaceted timing attributes, etc. The formal representation of these features is a challenging task. We explore the possibility of utilizing Event-B as a domain engineering tool. We discuss the problems we faced during this exercise and how we tackled them. Special attention is devoted to the issue of the validation of the model, in particular with a technique based on the animation of specifications. Event-B is mature enough to be an effective tool to model domains except in some areas, temporal properties mainly, where more work is still needed.
Type de document :
Article dans une revue
Requirements Engineering, Springer Verlag, 2011
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00590700
Contributeur : Atif Mashkoor <>
Soumis le : mercredi 4 mai 2011 - 17:19:30
Dernière modification le : jeudi 11 janvier 2018 - 06:20:08
Document(s) archivé(s) le : vendredi 5 août 2011 - 02:36:45

Fichier

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

Identifiants

  • HAL Id : inria-00590700, version 1

Collections

Citation

Atif Mashkoor, Jean-Pierre Jacquot. Utilizing Event-B for Domain Engineering: A Critical Analysis. Requirements Engineering, Springer Verlag, 2011. 〈inria-00590700〉

Partager

Métriques

Consultations de la notice

154

Téléchargements de fichiers

111