Abstract
Railway Transportation Management Systems are an emerging fi eld in the context of advanced distributed software systems.
Meth- ods 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 Traffi c Management System , aiming to
replace the diff erent 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 specifi cation of the standard. The model has been developed
through a sequence of model refi nement 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 diffi culties encountered in the specifi cation and during scenarios simulation.
[download the pdf file] [DOI]