Computer Science: Fully Funded EPSRC iCASE PhD Scholarship at Swansea University: Formal Modelling and Analysis of Real Time Systems
- Full cost of UK/EU tuition fees, plus a stipend
- 2 April 2018
Supervisor 1 Prof Markus Roggenbach (Swansea, UK)Supervisor 2 Dr Phillip James (Swansea, UK)
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.
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 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 systemsderive 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.
Work environment and supervision
The research project will take place within the Swansea Railway Verification Group (http://cs.swansea.ac.uk/rail/), which holds contacts to rail research groups in the UK and internationally. The supervisor team will include Dr M Seisenberger and Dr P D James, besides Prof M Roggenbach.
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. Science of Computer Programming 154 (2018) 61–88.
Candidates must have 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 a language like Maude or UPPAAL and/or testing would be welcome.
Due to funding restrictions, this studentship is open to UK/EU candidates only.
For candidates whose first language is not English, we require IELTS 6.5 (with 6.0 in each component) or equivalent. Please visit our website for a list of acceptable English language tests.
This three-year scholarship covers the full cost of UK/EU tuition fees, plus an annual stipend of £14,553.
Please visit our website for more information.
Sign Up for Scholarship Updates
Get an email every week that 10.000's of students use to get the latest scholarships.