Since each country has different requirements, operation rules and practices, the development of europe's railway results in a variety of different signaling and train control systems so far. When a train ran from Germany to France, it needs a replace of locomotive in order to fit the French signaling system and safety requirements, which may result in a high cost and potential hazards associated with safety.
In order to ensure interoperability in the European railway traffic, the Europe Train Control System (ETCS), as part of the Europe Rail Traffic Management System (ERTMS) has decided to replace all the existing conventional mainline signaling and control systems across Europe by ETCS equipments from 1996.
The ETCS needs a standard trackside equipment and a standard controller within the train cab. In its ultimate form, all the information is passed to the driver electronically instead of lineside signals.
However, for the on-board part of ETCS equipment, the degree of functional complexity has turned out to be significantly higher than that in national train control systems. Moreover, it results in a cost increase for software development and maintenance: ETCS standards, including requirements and architecture, are currently defined with natural languages. For this reason, the ETCS implementation and the related validation and verification are only internal to each providers and encapsulated for customers and public end users. This also leads to difficulty ensuring the quality of specifications and the consistency of various implementations.
In order to solve the problems mentioned above, a project OpenETCS is imposed. The aim of OpenETCS project is to "develop an integrated modeling, development, validation and testing framework for leveraging the cost-efficient and reliable implementation of ETCS".
In most cases, the reason for OpenETCS is not only to reduce the costs but also to reduce the strong dependence on the software producer. This is especially essential for technical software in the railway business, where equipment has been used for several decades and long-term support has to be ensured.
In my master's thesis and in cooperation with Deutsche Bahn Netz AG(a project leader of openETCS), a sub-component "Text Messages" of The Driver Machine Interfacer(DMI), which is a part of the openETCS onboard unit (OBU) model, has been modeled by means of a formal specification. The title is "Modeling, Verification and Validation of an On-Board-Unit for the European Train Control System"
Below is the simulation process of my modelling:
Below is the slides for my presentation of this master thesis: