The new CENELEC EN 50128 and the usedof formal method

The standard CENELEC 50128 [CEN 01, 11] identifies a complete process for software development of railway application. The new version 2011 introduced many new needs and a complete new structure. In this paper we present the new version of the CENELEC EN 50128 and describes how we can instantiate it. This new version introduce some new activities such the tools qualification, the software deployment, etc. and develop some activities such the data preparation and the software maintenance. In railway, we used from many year some formal methods for the specification, the conception and the verification by proof or model checking. This paper present the new CENELEC 50128 ([CEN 11]) and describe how the formal method can be used and what is impact on the recommended activities. 2