Abstract: “The use of formal methods in modeling and designing of railway transportation system is strongly recommended by CENELEC EN 50128 standart. Nowadays, the development of formal models of railway systems is completely performed manually. In this study, a software tool was developed by using C# programming language for automatic generation of the formal models of railway stations. The specially developed software tool generates the Timed-Arc Petri Net models, which is a formal method and highly recommended by the relevant standart, of the station components separately from the station topology.”

Keywords: formal methods; railway; automatic generation; station topolog