Citation

Boulanger JL. Rev. Electr. Electron. 2007; 2: 33-50.

Copyright

(Copyright © 2007, Societe de l' Electricite, de l' Electronique, et des Technologies de l' Information et de la Communication)

DOI

unavailable

PMID

unavailable

Abstract

Safety requirements are stringent in the railway environment. During the software development process, it is very important to keep these requirements traceable, even if the different models used are informal, semi-formal, or formal. This article reports on a study that investigated how the Unified Modeling Language (UML) can be used to formally specify and verify critical railway systems. The authors note that a benefit of using UML is its status as an international standard and its widespread use in the software industries. In this study, the authors propose a method for modeling a safety application for railways. The UML must be used with precise semantics, by definition of translation rules for the conversion of UML notation in a formal language. This study is integrated into a larger one (B-RAIL) that aims at linking an informal approach (UML notation) to a formal (B method) one. The authors designed a level crossing, without bridge or tunnel, to illustrate their method.