From UML to B - A level crossing case study

Abstract

The goal of this paper is to show how it is possible to combine the advantages of Unified Modelling Language (UML) and of the B method in order to design safety applications. We investigate how the Unified Modeling Langage (UML), can be used to formally specify and verify critical railways systems. A benefit of using UML is it status as an international standard (OMG) and its widespread use in the software industry. B is a formal method for the incremental development of specifications and their refinements down to an implementation. In the railway critical software domain, safety requirements are obviously severe. It is very important to keep requirements traceability during software development process even if the different used models are informal, semi formal or formal.