Schnieder, E.; Meyer zu Hörste, M.; Hungar, H.:
Modelling Functionality of Train Control Systems using Petri Nets.
Towards a Formal Methods Body of Knowledge for Railway Control and Safety Systems: FM-RAIL-BOK Workshop 2013, Madrid, Spain, September 2013.


Railway safety systems are highly complex systems with respect to functionality as well as dependability. The new European Train Control System (ETCS) as one part of the European Rail Traffic Management System (ERTMS) is the example presented here. A formal model using Coloured Petri Nets (CPN) was prepared by using the existing ERTMS/ETCS specification as a basis. The applied method is an integrated eventand data-oriented approach, which shows the different aspects of the system on their own Petri Net levels. The model comprises three sub-models with a model of the environment developed next to the onboard and trackside systems. This environment model covers all the additional systems connected through the system interfaces, examples of which are interlocking or regulation. Starting from a net representing the system context, the processes of the onboard and trackside sub-systems were modelled. Here, the different operations and processes are visualized in the form of scenarios, which in turn have access to additional refinements representing specific functions.