ASMs have been used at Siemens Corporate Technology to design a component in a software package called FALKO. Main purpose of FALKO is the construction and validation of timetables for railway systems. For simulation the whole closed-loop traffic control system is modelled within FALKO. The railway process model part of FALKO was formally specified using the ASM approach. C++ code is generated from the formal specification and compiled together with the handwritten C++ code of the other components to obtain the FALKO executable. The project started in May 1998 and was finished in March 1999. Since then FALKO is used by the Vienna Subway Operator for the validation of the whole subway operational service. 1 FALKO Abstract State Machines (ASMs) [Gur95,BH98] have been used at Siemens Corporate Technology to design a component in a software package called FALKO. This name is the German acronym for “Timetable Validation and Timetable Construction” describing concisely the main functi...