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.