A formal design of the hybrid European rail traffic management system

Railway Transportation Management Systems are an emerging field in the context of advanced distributed software systems. Methods and techniques supporting rigorous formal design of system architecture where software components interact with each other and control physical components are highly demanded to assure reliability of the system operation. We present a formal model of the Hybrid ERTMS/ETCS Level 3, the new standard of the European Rail Traffic Management System, aiming to replace the different national train control and command systems by a unique European railway management system. We use the Abstract State Machine (ASM) formal method to provide a complete specification of the standard. The model has been developed through a sequence of model refinement steps following the incremental way in which requirements describe train operation. We have exploited the ASMETA tool-set supporting the ASMs to simulate the abstract models and validate them with respect to the operational scenarios that are given as part of the requirements. We discuss ambiguities and inconsistencies of the requirements, as well as difficulties encountered in the specification and during scenarios simulation.