Overcoming the railway capacity challenges without undermining rail network safety (SafeCap)

The overall aim of this project is to develop modelling techniques and tools for improving railway capacity while ensuring that safety standards are maintained.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 distances 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.To achieve our overall aim of improving railway capacity, we intend to meet the following technological (T) and scientific (S) and objectives:1) 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).2) To develop an intuitive graphical domain-specific language for the railway domain with a tailored tool support based on the Rodin framework (T)3) 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 the project team with 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.

The overall goal of the SafeCap project is to provide an enhanced railway service to end users (i.e., passengers). We have identified the following three major beneficiaries: - Invensys Rail (project partner), - the railway industry, and - the industrial sectors working on developing control systems. The SafeCap project will develop technologies universally applicable to the railway domain. For this purpose, every effort will be made to ensure technology transfer to Invensys Rail. At the same time, the project will tackle general problems of rigorous modelling and verification of complex real-time control systems. Invensys Rail will gain understanding and techniques to enable simultaneous reasoning about railway capacity and safety. This means that new techniques for increasing capacity can be evaluated with a guarantee that fundamental railway safety properties, such as separation of trains, can be verified. Secondly, Invensys Rail will aim to apply the specific capacity enhancements discovered during the project to signalling schemes, both in the UK and potentially across the Invensys Rail customer base worldwide. Some of the methods of increasing capacity may challenge traditional signalling principles. In these cases, the ability to demonstrate that the fundamental railway safety properties are still ensured will be an important factor in any decision to use the new methods. The uptake by industry will require discussion with Invensys Rail customers as well as with safety assessors working for Invensys Rail directly or for Invensys Rail customers. Railway industry. The main aim of the project is to develop capacity-enhancing technologies which are generally transferable to the railway domain. Companies working in this domain will be able to adopt the technologies to be developed in SafeCap by setting up concrete technology transfer projects intended to - adjust the developed solutions to their specific languages - integrate the new tools in their tool environments - train their engineers. Industrial sectors working on developing control systems. The problems of reasoning about time in the course of system modelling and of smoothly integrating functional and timed modelling are general for all control systems. SafeCap builds on general methods and tools applicable to a wide variety of control systems. For example, various companies from the space, transportation and automotive domains are now working on transferring newly-developed Event-B technologies; extending these technologies with reasoning about time will add a further crucial dimension.