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.
Organisations
- Newcastle University (Lead Research Organisation)
- Rail Safety and Standards Board (United Kingdom) (Co-funder)
- University of Augsburg (Collaboration)
- ClearSy (Collaboration)
- Siemens AG (Collaboration)
- University of Surrey (Collaboration)
- University of Bremen (Collaboration)
- Heinrich Heine University Düsseldorf (Collaboration)
- Invensys Rail (Collaboration)
- National Institute of Advanced Industrial Science and Technology (Project Partner)
- Invensys Rail Ltd (Project Partner)
Publications
Alexander Romanovsky (Author)
(2012)
The SafeCap toolset for improving railway capacity while ensuring its safety.
Allen A
(2022)
Developing a well-received pre-matriculation program: the evolution of MedFIT.
in Discover education
Isobe Y
(2012)
Integrated Formal Methods
James P
(2013)
Hardware and Software: Verification and Testing
James P
(2013)
NASA Formal Methods
James P
(2014)
Techniques for modelling and verifying railway interlockings
in International Journal on Software Tools for Technology Transfer
James P
(2014)
On modelling and verifying railway interlockings: Tracking train lengths
in Science of Computer Programming
Markus Roggenbach (Co-Author)
(2013)
Verification of Scheme Plans using CSP||B
Markus Roggenbach (Co-Author)
(2012)
Railway modelling in CSP||B: the double junction case study
Markus Roggenbach (Co-Author)
(2011)
A Simulator for Timed CSP
Markus Roggenbach (Co-Author)
(2013)
Verification of solid state interlocking programs
Markus Roggenbach (Co-Author)
(2012)
Timed CSP Simulator
Markus Roggenbach (Co-Author)
(2011)
Designing Domain Specific Languages for Verification: First Steps
Markus Roggenbach (Co-Author)
(2012)
Using CSP||B and ProB for railway modelling
Moller F
(2013)
Hardware and Software: Verification and Testing
Description | This work created the foundation for developing rigorous and scalable techniques and tools enabling practical automated verification of signalling and interlocking safety. |
Exploitation Route | This work paves the foundation for creating practical safety verification techniques that are easy to deploy in railway companies without serious extra investment and disturbing the current practices. |
Sectors | Transport |
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 (now Siemens Rail Automation), 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. |
First Year Of Impact | 2014 |
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 | Public |
Country | United Kingdom |
Start | 05/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. |
Collaborator Contribution | The partner bring into this cooperation the knowledge of the French railway sector and their successful experience in applying formal methods in the domain. |
Impact | We have lunched together a very successful International Conference on reliability, safety and security of railway systems: modelling, analysis, verification and certification (RSSRail). The 3rd edition RSSRail 2019 was held in June 2019 in Lille. |
Start Year | 2012 |
Description | Cooperation with Siemens Rail Automation |
Organisation | Invensys Rail |
Country | United Kingdom |
Sector | Private |
PI Contribution | We are developing new methods for engineering trustworthy advisory systems for railway traffic management. Our team contributes the expertise in trustworthy system engineering and in requirement engineering. |
Collaborator Contribution | Feedback and advice on the research results developed |
Impact | No outputs at this stage except for a number of publications. But the work on developing novel practical techniques for safety verification is successfully moving forward. |
Start Year | 2012 |
Description | Development of an advanced railway advisory system |
Organisation | Siemens AG |
Department | Siemens Rail Automation |
Country | Global |
Sector | Private |
PI Contribution | Our team work on developing the foundations of the advisory system (architecture, algorithms, components). |
Collaborator Contribution | The partners help us by providing feedback, expert knowledge, case studies. |
Impact | Too early to report. |
Start Year | 2013 |
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. Among other functionalities the toolset supports scalable fully-automated verification of railway signalling/interlocking and is easy to integrate into the current development processes in the railway companies. |
Type Of Technology | Software |
Year Produced | 2013 |
Open Source License? | Yes |
Impact | SafeCap is an Eclipse-based toolset for entering and analysing railway junction schemas. The toolset 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. Among other functionalities the toolset supports scalable fully-automated verification of railway signalling/interlocking. This version of the toolset targets the signalling designed in the standard digital notations (SSI, SDEF, RailML, et.) used in the industry and is easy to integrate into the current development processes in the railway companies. In 2019 the toolset was approved for the use for formal verification of signalling in the UK for and has been used by several major railway companies in the country. |
URL | https://safecap.co.uk/ |
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 |
Geographic Reach | International |
Primary Audience | Professional Practitioners |
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,2014,2015,2016 |
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 | Industry/Business |
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 |
Geographic Reach | National |
Primary Audience | Professional Practitioners |
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 |
Description | The SafeCap toolset for improving railway capacity while ensuring its safety |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | Yes |
Geographic Reach | National |
Primary Audience | Professional Practitioners |
Results and Impact | Presentation at the 1st Rail Research UK Association (RRUKA) Annual Conference. This presentation reported on the RSSB/EPSRC UK SafeCap project that developed modelling techniques and tools for improving railway capacity while ensuring that safety standards are maintained. The presentation and the accompanying paper reported on the SafeCap results on designing a Domain Specific Language (DSL), a verification infrastructure and the approaches to estimating and improving capacity. |
Year(s) Of Engagement Activity | 2012 |
URL | http://rruka.org.uk/rruka-annual-conference-2012-conference-proceedings/ |