From February 2011 to May 2013
Project Leader(s): Prof. Sascha Romanovsky
Staff: Dr. Alex Iliasov, Ilya Lopatkin
Contact: Prof. Sascha Romanovsky
Sponsors: EPSRC, RSSB
Partners: Swansea University, Invensys Rail Ltd, AIST
The overall aim of this project is to develop modelling techniques and tools for improving railway capacity while ensuring that safety standards are maintained. To achieve this aim we set out to meet the following scientific and technological objectives: (i) - to integrate proof-based reasoning about time in the state-based models exemplified by Event-B and CSP-Prover, and to provide open tool support for verifying timed systems. (ii) - to develop an intuitive graphical domain-specific language for the railway domain with tailored tool support based on the RODIN framework. (iii) - to identify and validate design patterns for improving capacity by altering route design, track layout, signalling principles and driving rules.
The tool support will allow the user to vary parameters such as route design, track layout and signalling, rolling stock capacity and operational parameters to achieve improvement in capacity without undermining the system safety. Starting with the solid basis of Invensys' engineering expertise, we will take a radical approach and "think the unthinkable" (for the conservative railway domain); the tool developed will provide the necessary feedback to allow us to push the boundaries of what can be achieved.
Overall, by allowing companies working on the development of rail control and communication solutions to optimize their solutions, the project results will improve railway capacity without compromising safety. These companies will be able to use novel technologies based on advanced formal modelling and strong tool support developed within the project. The technologies will incorporate domain-specific graphical notations and an advanced tool environment, with automated reasoning about the timed properties of the railway systems under development hidden from engineers.
Follow the SafeCap Platform development at Source Forge.