Formalization and validation of a subset of the European Train Control System

The European Train Control System (ETCS) is a control system for the interoperability of the railways across Europe. In this paper, we report on the activities of the EuRailCheck project, promoted by the European Railway Agency, for the development of a methodology and tools for the formalization and validation of the ETCS specifications. Within the project, we achieved three main results. First, we developed a methodology for the formalization and validation of the ETCS specifications. The methodology is based on a three-phases approach that goes from the informal analysis of the requirements, to their formalization and validation. Second, we developed a set of support tools, covering the various phases of the methodology. Third, we formalized a realistic subset of the specification in an industrial setting. The results of the project were positively evaluated by domain experts from different manufacturing and railway companies.