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.