Fully Funded EPSRC iCASE PhD Scholarship: Formal Modelling and Analysis of Real Time Systems

This project is suitable for candidates interested in Formal Methods and working together with an industrial company. This is an EPSRC funded iCASE PhD project for 4 years, partially funded by the company Siemens.

Background

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.

Preliminary work

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.

Originally arising from an EPSRC/Siemens-funded PhD project undertaken by Dr Andrew Lawrence at Swansea University, this work has lead within the academic context to a number of well-recognised publications. Dr Lawrence has subsequently been hired as a software engineer by Siemens UK in Chippenham.

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:

- provide for this design a formally verified, location-specific test model;
- develop a test theory for testing real time systems
- derive test suites according to the test theory from the developed 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.

Suggested programme of work

To achieve these objectives, we suggest the following as a programme of work:

- Provide an automatic translation between messages in the model and the messages exchanged over the interfaces of Siemens Interlocking and RBC.
- Address the problem of scalability by verifying large examples.
- Develop a testing approach that realises an adequate conformance relation between the formal model and the Siemens ERTMS components.
- Deploy the developed technology within Siemens, Chippenham.

For this programme it is helpful that EPSRC CASE studentships include longer periods of time during which the PhD candidate will work within Siemens. This will ease the necessary technical discussion, e.g., on the interfaces of the Siemens components, on finding an adequate notion of conformance, and especially on deployment.

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

Eligibility:
Candidates should hold a first, upper second class honours or a master’s degree (with Merit), in Computer Science or equivalent.

A solid background in Formal Methods will be required; knowledge in a language Maude or UPPAAL and/or testing would be welcome.

Due to funding restrictions, this studentship is open to UK/EU candidates only.