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.
(2019). A formal design of the hybrid European rail traffic management system . Retrieved from http://hdl.handle.net/10446/151158
A formal design of the hybrid European rail traffic management system
Gargantini, Angelo
2019-01-01
Abstract
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.File | Dimensione del file | Formato | |
---|---|---|---|
faacs_camerready.pdf
Solo gestori di archivio
Versione:
publisher's version - versione editoriale
Licenza:
Licenza default Aisberg
Dimensione del file
970.09 kB
Formato
Adobe PDF
|
970.09 kB | Adobe PDF | Visualizza/Apri |
Pubblicazioni consigliate
Aisberg ©2008 Servizi bibliotecari, Università degli studi di Bergamo | Terms of use/Condizioni di utilizzo