Safecap Project Wiki
From Safecap Wiki
PhD Studentship available
Industrial conversion Computer Science PhD studentship in developing train advisory systems of the future.
We have a PhD studentship jointly supported by EPSRC and Siemens Rail Automation. The aim is to develop advanced computer science techniques for analysing real-time safety, capacity and energy consumption in train advisory systems.
The study will be conducted at the School of Computing Science of Newcastle University () in close cooperation with engineers from Siemens Rail Automation. The student will learn about the advanced technologies used by a world-leading railway company and spend 3-4 months' time working in the company environment. This study is part of the research conducted by the School’s Dependability Group in the area of railway modelling ().
The relevant areas of computer science are software engineering, formal methods, verification, discrete modelling, safety analysis, high-performance computation, multi-processors/many-cores and system optimisation.
This is a 3.5 years PhD study with a £17.790 annual stipend. The fee is fully covered by the grant.
Only UK applicants and EU applicants who have been ordinarily resident in the UK for 3 years are eligible. The ideal candidates will hold a first or high second degree (MSc level is a plus) in computer science or a closely related discipline. The study will start in January 2014.
Please apply by November 30 2013. You must apply through the University's online postgraduate application form inserting the reference number CS044 and selecting 'PhD COMP', with programme code 8050F, as the programme of study. You should also send your covering letter and CV by e-mail to Catherine McAndrew (), Postgraduate Secretary, School of Computing Science, Faculty of Science, Agriculture and Engineering, Newcastle University, Newcastle upon Tyne, NE1 7AD
Potential candidates are welcome to discuss their applications informally with Prof Alexander Romanovsky ().
The overall aim of the SafeCap project is to develop modelling techniques and tools for improving railway capacity while ensuring that safety standards are maintained.
To achieve our overall aim of improving railway capacity, we intend to meet the following technological (T) and scientific (S) objectives:
- To integrate proof-based reasoning about time in state-based models, exemplified by Event-B and CSP-Prover, and to provide an open tool support for verifying timed systems (S).
- To develop an intuitive graphical domain-specific language for the railway domain with a tailored tool support based on the Rodin framework (T)
- To identify and validate design patterns for improving capacity by altering route design, track layout, signalling principles and driving rules (T)
Throughout the project, our industrial partner Invensys Rail will provide track plans and control software, which will be used as case studies in order to challenge our approach with realistic data sets. Regular meetings and workshops involving Invensys Rail will give the practical feedback necessary to come up with solutions which are viable for the rail industry. Invensys Rail’s successful experience of improving the capacity of metro railways by using smarter control solutions will be an invaluable contribution to this work.
The results of the project will be used to evaluate the viability of approaches to improving railway capacity and to prepare the deployment of the developed solutions in the railway industry.
SafeCap is run from January 2011 to August 2013.
The railway domain has been identified as a grand challenge for computer science. Due to its safety-critical nature, various formal methods have been applied in this domain, where, most prominently, the B method has been successfully used to verify several lines, including those in Paris and San Juan Metro. Solely concerned with safety, most approaches have, however, ignored the aspect of time. Furthermore, a rigorous treatment of time is widely recognised as a challenge in its own right by the computer science community.
And yet the capacity of a rail network node is highly dependent on time: moving a point or a train through a node takes time, and sighting and braking distance are functions of time. This is why we propose extending Event-B, a modern variant of the B method, with reasoning about time and underpinning it with various tools for simulation, analysis and verification. To this end, we will integrate Event-B with process algebra CSP. This will make it possible to re-use proof support developed for CSP. Overall, our approach will allow an integrated view of rail networks, within which capacity can be investigated without compromising safety.
In our project, we will handle time precisely, i.e. without any rounding errors. In simulations, this can be achieved by using the rationals in the language Haskell; in proofs, the theorem prover Isabelle/HOL includes proper real numbers (as well as rationals). We will extend the interactive proof tool CSP-Prover and build a new tool support. By relying on such tool support, the railway engineer will be able to model and evaluate the impact on capacity of altering track layouts, signalling principles, driving rules and control algorithms. By integrating our tool into the Event-B tool environment, our project will deliver a software development platform that would allow engineers to model, simulate, analyse and verify railway network nodes (both junctions and stations) in an integrated way, combining reasoning about capacity and safety.
Follow the development of the SafeCap Platform at our Sourceforge site.
Partners and People
The following organisations and people are co-operating for the SafeCap project:
People at Invensys Rail: Domenic Taylor, Simon Chadwick.
People at AIST: Yoshi Isobe.
For more details please contact: Alexander Romanovsky