Swansea University is a UK top 30 institution for research excellence (Research Excellence Framework 2014), and has been named Welsh University of the Year 2017 by The Times and Sunday Times Good University Guide.
This is an EPSRC funded iCASE PhD project for 4 years. The PhD project is partially funded by the company Siemens.
Start date: 25 September 2017
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.
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 [1,2,3]. Dr Lawrence has subsequently been hired as a software engineer by Siemens UK in Chippenham.
Given a location-specific design for an ERTMS-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;
- 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.
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.
1. A. Lawrence, U. Berger, P. James, M. Roggenbach, and M. Seisenberger. Modelling and analysing the European Rail Traffic Management System in Real-Time Maude. In FTSCS’14 – Preliminary Proceedings, 2014.
2. P. James, A. Lawrence, M. Roggenbach, and M. Seisenberger. Towards safety analysis of ERTMS/ETCS level 2 in Real-Time Maude. In C. Artho and P.C.Olveczky, editors, Formal Techniques for Safety-Critical Systems - Fourth International Workshop, FTSCS 2015, Paris, France, November 6-7, 2015. Revised Selected Papers, volume 596 of Communications in Computer and Information Science, pages 103–120. Springer, 2015.
3. Ulrich Berger, Phillip James, Andrew Lawrence, Markus Roggenbach, Monika Seisenberger. Verification of the European Rail Traffic Management System in Real-Time Maude. 31 pages. Submitted to an International Journal.
Candidates should hold a first, upper second class honours or a Masters degree (with Merit), in Computer Science or equivalent.
A solid background in Formal Methods will be required; knowledge in Maude and/or testing would be welcome.
Due to funding restrictions, this studentship is open to UK/EU candidates only.
The studentship covers the full cost of UK/EU tuition fees, plus an annual stipend of £14,553.
There will be funds for other expenses and the grant includes funding for staying longer periods of time at the Siemens, Chippenham, UK.