Analysis and Formal Modeling of Systems Behavior Using UML/Event-B
| Autor: | Philippe Bon, Rahma Ben Ayed, Simon Collard-Dutilleul, Kenza Kraibi, Dorian Peit |
|---|---|
| Přispěvatelé: | Institut de Recherche Technologique Railenium, Évaluation des Systèmes de Transports Automatisés et de leur Sécurité (IFSTTAR/COSYS/ESTAS), Institut Français des Sciences et Technologies des Transports, de l'Aménagement et des Réseaux (IFSTTAR)-PRES Université Lille Nord de France, Laboratoire d'Automatique, de Mécanique et d'Informatique industrielles et Humaines - UMR 8201 (LAMIH), INSA Institut National des Sciences Appliquées Hauts-de-France (INSA Hauts-De-France)-Centre National de la Recherche Scientifique (CNRS)-Université de Valenciennes et du Hainaut-Cambrésis (UVHC) |
| Rok vydání: | 2019 |
| Předmět: |
MODELE MATHEMATIQUE
[INFO.INFO-SC]Computer Science [cs]/Symbolic Computation [cs.SC] RAILWAY SIGNALING METHODE FORMELLE Programming language Computer science 020207 software engineering 02 engineering and technology computer.software_genre MODELISATION UML SYSTEME CRITIQUE Unified Modeling Language FORMAL VERIFICATION SAFETY EVENT-B 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing SECURITE computer BEHAVIOR computer.programming_language |
| Zdroj: | journal of communications journal of communications, 2019, 14 (10), pp980-986. ⟨10.12720/jcm.14.10.980-986⟩ |
| ISSN: | 2374-4367 |
| DOI: | 10.12720/jcm.14.10.980-986 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|