Home > Published Issues > 2019 > Volume 14, No. 10, October 2019 >

Analysis and Formal Modeling of Systems Behavior Using UML/Event-B

Kenza Kraibi1, Rahma Ben Ayed 2, Simon Collard-Dutilleul1,2, Philippe Bon1,2, Dorian PEIT1,3
1. Institut de Recherche Technologique Railenium, F-59300, Famars, France
2. IFSTTAR-COSYS-ESTAS, F-59666, Villeneuve d’Ascq, France
3. Université Polytechnique Hauts-de-France, LAMIH UMR CNRS 8201, F-59313 Valenciennes, France

Abstract—The verification of safety properties of critical systems, such as railway signaling systems, is better achieved by formal reasoning. Event-B as a formal method, allows to get safe and reliable systems. Nevertheless, modeling with Event-B method requires some knowledge on mathematical logic and set theory. In opposition, UML (Unified Modeling Language) is a commonly used graphical language, but it does not guarantee the verification of safety properties. This paper presents an approach combining UML and Event-B. In fact, we focus in this work on modeling the systems behavior with the joint use of some UML behavioral diagrams. The UML models are then translated into Event-B models for the systems validation as well as the verification of safety properties using B tools. This methodology is illustrated by an application on a case study of railway signaling system.

Index Terms—Event-B, UML, behavior, formal verification, safety, railway signaling.

Cite: Kenza Kraibi, Rahma Ben Ayed, Simon Collard-Dutilleul, Philippe Bon, and Dorian PEIT, “Analysis and Formal Modeling of Systems Behavior Using UML/Event-B,” vol. 14, no. 10, pp. 980-986, 2019. Doi: 10.12720/jcm.14.10.980-986.