Author(s)

J.-L. Boulanger, P. Bon & G. Mariano

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. Keywords: B method, formal development, level crossing, software verification. 1 Introduction In spite of progress carried out in software development, designing a complex system while respecting its safety requirements, remains very hard. During the critical software development process, safety and security requirements must be traced from informal specification to code generation. So we need to trace them in the different models: informal, semi formal or formal ones. We present a new method here to transform a semi formal modelling to a formal specification which enables them to be traced. This method will be applied to a railways case study, where safety requirements are very strict. We study a level crossing case study taking into account French particularities. This article is made up 3 parts. Firstly, we describe the case study. In the following part we present the principles of UML and we give a part of semi formal modelling of the level crossing. In the last part

Keywords

B method, formal development, level crossing, software verification.