Testing from verified test-models for ERMTS level 2

The ERTMS Train Control System is a state-of-the-art system designed
as a standard for railways across Europe. While the ERTMS standard
details the interactions between trains and track equipment (e.g., in
order to obtain concise train position information) and a radio block
centre and trains (e.g., to hand out movement authorities), the
details of how the controller, the interlocking and the radio block
centre interact with each other are left to the suppliers of
signalling solutions.

Over the last four years, Siemens Rail Automation UK and Swansea
University have co-operated on the development of a formal model of
ERTMS level 2 as realised by Siemens. To the best of our knowledge,
this work presents the first and currently only formal ERTMS model
that encompasses all of the ERTMS subsystems required for the full
control cycle. The model either provides a formal argument that a
given detailed design is safe, or it gives a counter example trace
illustrating a sequence of events that leads to an unsafe situation.

Objectives

This PhD project sets out to achieve the following objectives:

Given a location-specific design for an ERMTS-controlled rail yard,
i.e., interlocking tables and rules as to what messages the radio
block centre (RBC) shall send in different situations:

[O1] to provide for this design a formally verified,
location-specific test model;

[O2] to derive test suites from this test model with which the
location-specific Siemens RBC realisation and/or the location-specific
interlocking computer can be tested - either in isolation or in
combination with each other.

Time permitting, the last phase of the project could be on scoping
how to extend this work to ERTMS level.

Potential applications and benefits

Railways in the UK - and worldwide - are experiencing ever more
intensive use of their services, as the demand for rail transport
modes increases. As this happens, the existing railway infrastructure
is becoming more and more overloaded. Because of this, the problem of
increasing the capacity of the nation's rail system is becoming a
significant challenge in the UK as well as elsewhere.

One straightforward way to increase railway capacity is to simply
build more railway tracks; e.g., High Speed Two (HS2) and Crossrail
provide two such high-profile solutions, the former for mainline rail
network and the latter for London metro. However, this is a very
expensive solution which is typically faced with insurmountable
obstacles, such as the mere lack of space and the presence of listed
buildings. What is really needed, then, are ways to increase the
capacity of the existing rail network. To this end, upgrading
signalling and train control systems is regarded as a cost efficient
way to increase the capacity in existing railway - and at the same
time decrease energy consumption.

The European Train Control System of the European Rail Traffic
Management System (ERTMS-ETCS) has been proposed to do just this:
classical traffic light signalling is replaced by communication
between a central unit and the trains. This project sets out to
improve quality assurance for ERTMS-ETCS by the use of formal
methods.

When completed, this PhD project will contribute to Siemens Rail
UK quality assurance processes and bring benefits in terms of quality,
time and cost. Beyond Siemens Rail UK, this could lead to a culture
change within the railway industry, in particular with respect to
standards and contracts for development. Furthermore, there is hope
for a wider societal impact concerning adaption of formal methods.

Alignment to EPSRC research areas

This PhD project directly addresses two out of the four themes set out
by EPSRC in their vision ""Science for a successful nation"":
""Productive nation"", as the proposal directly reacts to research needs
from Siemens Rail UK; and ""Resilient nation"" as it explicitly refers
to the smooth a