with the support of ITEA

Excerpt from the openETCS website.

openETCS is a project, not an organisation. The goal of the project is an “Open Proof” for the European Train Control System.

The Context

Europe’s railways have developed over the last 150 years within national boundaries, resulting in a variety of different signalling and train control systems, which hampers cross-border traffic. The European Union has decided to improve interoperability for the railway sector. Therefore the European Train Control System (ETCS) as part of the European Rail Traffic Management System (ERTMS) is intended to replace almost all national legacy mainline signalling and train control systems all across Europe. ETCS consists of infrastructure components and on-board units (OBU). A System Requirement Specification (SRS, actual Version: 2.3.0d) has been cooperatively created mainly by 6 major European railway signalling manufacturers. Those firms have formed an association, called UNISIG to manage and coordinate these activities in close cooperation with the EU Commission and the bodies of railway operators. Beginning with the 3rd version of the SRS, this document has been published by the European Railway Agency (ERA), therefore in the“public domain” and will be mandatory by 2015 for all new infrastructure and train borne signalling and train control equipment.

Especially for the on-board part of the ETCS equipment the degree of functional complexity to be implemented has turned out to be significantly higher than in conventional signalling and train control systems, thus resulting in significant cost increases for software development, homologation and maintenance. This has caused a cost level for the operators, which is by a factor of 3 to 10 times higher compared with conventional national onboard systems at the same overall performance level.

The Goals and major expected outcomes

The purpose of the openETCS project is to develop an integrated modelling, development, validation and testing framework for leveraging the cost-efficient and reliable implementation of ETCS. The framework will provide a holistic tool chain across the whole development process of ETCS software. The tool chain will support the formal specification and verification of the ETCS system requirements, the automatic and ETCS compliant code generation and validation, and the model-based test case generation and execution. openETCS will utilize “Open Standards” on all levels, including hardware and software specifica­tion, interface definition, design tools, verification and validation procedures and last but not least embedded control software. By applying those technologies and related business concepts a significant cost cut for the final onboard product is expected down to or even below conventional high performance cab signalling systems (e.g. LZB Linien-Zug-Beeinflussung, as used in Germany, Austria and Spain). The open source concept provides for a neutral and formal method based “correct” functioning reference device that will help to overcome existing interoperability problems, supporting manufacturers, infrastructure managers and railway undertakings alike, avoiding exhaustive field tests, transferring verification and validation activities from the track site into laboratories, saving scarce resources and finally accelerating the migration phase and therefore supporting the European ERTMS deployment plan.

CNRS Researcher

My research interests include formal methods and concurrency semantics.


Real-Time Model Checking Support for AADL

We describe a model-checking toolchain for the behavioral verification of AADL models that takes into account the realtime …

Time Petri Nets with Dynamic Firing Dates: Semantics and Applications

We define an extension of time Petri nets such that the time at which a transition can fire, also called its firing date, may be …

Model-Checking Real-Time Properties of an Aircraft Landing Gear System Using Fiacre

We describe our experience with modeling the landing gear system of an aircraft using the formal specification language Fiacre. …

Time Petri nets with dynamic firing dates: semantics and applications

We define an extension of time Petri nets such that the time at which a transition can fire, also called its firing date, may be …