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

Lead Research Organisation: Newcastle University
Department Name: Computing Sciences

Abstract

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.

Planned Impact

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.

Publications

10 25 50
 
Description Our work impacts current practices and strategic planning within the Railway Industry. • current practices: it has led to the adoption of formal verification techniques at Invensys Rail, a multi-national technology leader, as well as operational and structural changes (personnel and thinking) in the company. • strategic planning: addressing the problem of the adoption of the European Train Management System (ERTMS) in the UK as a replacement for traditional interlocking, our research produces data in support of change, and involves us in various working groups and initiatives developing national policy for the development of the UK railway. Beneficiaries: UK railway industry
Sector Transport
Impact Types Societal,Economic

 
Description Ensuring the industrial application of the SafeCap technology (SafeCap-Impact)
Amount £79,622 (GBP)
Funding ID EP/K503885/1 
Organisation Engineering and Physical Sciences Research Council (EPSRC) 
Sector Academic/University
Country United Kingdom
Start 06/2013 
End 08/2014
 
Description Railway Control Systems
Amount £103,500 (GBP)
Organisation Invensys Rail 
Sector Private
Country United Kingdom
Start 01/2008 
End 01/2014
 
Description Cooperation with ClearSy 
Organisation ClearSy
Country France 
Sector Private 
PI Contribution We have established a close cooperation with ClearSy (French SME working in railway domain, http://www.clearsy.com/). The cooperation plans include tool integration, joint project proposals, and staff visits.
Start Year 2012
 
Description Formalizing domain specific languages using UML 
Organisation University of Augsburg
Country Germany 
Sector Academic/University 
PI Contribution This work bridges the gap between an industrial data model and a formal specification necessary for reasoning. It presents the first UML Class Diagram Institution capable of practical use. Our methods use institution co-morphisms to combine UML Class Diagrams with ANY formalisim describing system evolution, e.g., UML Statecharts or UML Sequence Diagrams; we exemplify them with Modal-CASL and CASL. Results contribute to an international effort to formalize the relation between UML diagrams. The data model is Siemens-Invensys for rail signalling, based on UML class diagrams accompanied with natural language descriptions, intended to unify Internationals Standards that use 6 primary description notations.
Start Year 2011
 
Description Institution Theory 
Organisation University of Bremen
Country Germany 
Sector Academic/University 
PI Contribution In order to ensure that the translations from UML diagrams into formal specification languages such as CASL and ModalCASL are semantics preserving, we work within the framework of institutions. This allows to prove semantic equivalence between specifications written in different formalisms.
Start Year 1998
 
Description Railway modelling and verification with University of Surrey 
Organisation University of Surrey
Department Department of Computing
Country United Kingdom 
Sector Academic/University 
PI Contribution In this collaboration, partners from Surrey, Swansea, and Invensys Rail developed a formal model of Railway Interlockings in the language CSP||B. This modelling turns out to be "natural" in the sense that rail engineers can understand it. Furthermore, verification for safety can practically performed, thanks to a number of proof techniques developed. The open OnTrack tooling environment supports the automated modelling and verifying of Railway Scheme Plans. Beyond the SafeCap project, we plan to further develop the OnTrack tool and to apply our modelling approach in to ETCS railway systems.
Start Year 2011
 
Description Tooling with ProB 
Organisation Heinrich Heine University Düsseldorf
Country Germany 
Sector Academic/University 
PI Contribution Timed CSP Simulator, one of the research outputs of the SafeCap project, is built on top of the CSP Simulator of the tool ProB. In this cooperation, we discussed technicalities on how to extend the existing software in the best way.
Start Year 2011
 
Title The SafeCap toolset for improving railway capacity while ensuring its safety 
Description Safecap is an Eclipse-based tool for entering and analysing railway junction schemas. The tool aims to be extensible and configurable and may be applied in a number of contexts such the analysis of control table for junction signals, assessment of capacity impact of signal positioning and train detection circuit boundaries, and also for conducting semi-automatic or automatic changes to schema topology or control tables. 
Type Of Technology Software 
Year Produced 2013 
URL http://safecap.sourceforge.net/
 
Description SafeCap toolset - YouTube video 
Form Of Engagement Activity A press release, press conference or response to a media enquiry/interview
Part Of Official Scheme? Yes
Primary Audience
Results and Impact pubic video describing the essence of the SafeCap method and tools:



http://www.youtube.com/watch?v=HBefIPSR_Z8.

video
Year(s) Of Engagement Activity 2013
URL http://www.youtube.com/watch?v=HBefIPSR_Z8
 
Description SafeCap: advanced computer science techniques for railways of tomorrow. 
Form Of Engagement Activity A magazine, newsletter or online publication
Part Of Official Scheme? Yes
Geographic Reach International
Primary Audience
Results and Impact A paper written for the European policymakers and published in the EURAILmag Magazine.

Alexei Iliasov, Ilya Lopatkin, Alexander Romanovsky. SafeCap: advanced computer science techniques for railways of tomorrow. EURAILmag. Issue 28. September. 2013. (http://eurailmag.com/)
Year(s) Of Engagement Activity 2013
 
Description The Future of Train Control Systems 
Form Of Engagement Activity A formal working group, expert panel or dialogue
Part Of Official Scheme? No
Primary Audience
Results and Impact This paper gives an overview of the contribution of university-based research to the future development of train control and communications systems. Specifically it provides insight into research being conducted by UK universities to support the development of new train control systems, and includes some of the more radical ideas being investigated.

The Future of Train Control Systems: a Technical Paper presenting the contribution of university-based research to the future development of train control and communications systems.



http://www.irse.org/events
Year(s) Of Engagement Activity 2013