Domain Engineering with Event-B: Some Lessons We Learned

Atif Mashkoor (1) , Jean-Pierre Jacquot (1)

1 DEDALE - Development of specifications

Well specified requirements are crucial for good software design and domain engineering helps better understanding and specification of requirements. Safety critical domains, such as 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. This paper presents our experience of modeling land transportation domain in the formal framework of Event-B. We explore the possibility of using Event-B as a domain engineering tool. We discuss the problems posed by the introduction of time and how we tackle it. We design a technique based on animation to validate domain models.

Mots clés: Domain engineering; Formal methodes; Event-B : Animation; Brama

Domaines: Génie logiciel [cs.SE]

Atif Mashkoor, Jean-Pierre Jacquot. Domain Engineering with Event-B: Some Lessons We Learned. 18th International Requirements Engineering Conference - RE'10, Sep 2010, Sydney, Australia. pp.252 - 261, ⟨10.1109/RE.2010.37⟩. ⟨inria-00431133v2⟩