ABSTRACT
The dependability assessment of systems and in particular their availability depends on the dysfunctional behaviors and maintenance policies of their subsystems and components. Railway systems are large due to the number of trains and routes but also complex due to the safety assured by the signaling and the interlocking. There is a need of methods and tools which could give, at the same time to people in charge of the design, operation and maintenance, the key to exploit the infrastructure at the best cost. The aim of this paper is to present a methodology to evaluate the performance of railway systems and relevant for the different department of a railway company. It is shown that functional and dysfunctional specifications can be proved formally and then used to generate large formal models in the form of colored Petri Net, and this in an automatic way. After simulation, various metrics can then be extracted like the dependability of components, the capacity of a track or the needs of maintenance.
