Theories, techniques and tools for engineering

Lead Research Organisation: Newcastle University
Department Name: Computing Sciences

Abstract

Railway networks use a range of different signalling principles, for example route-based signalling, speed signalling, signalling using train protection systems such as the different levels of the European Train Control System, and Communication Based Train Control. Cost and practical constraints mean that there is a limit to the amount of each network that can be changed from one system to another in a given time period, as a result of which it is inevitable that networks use a mixture of signalling systems.

There is no single theory for rigorous analysis and simulation of such mixed systems, leading to a strong dependence on engineering judgement. This has the potential to lead to either over-design or accidental restrictions in capacity. In the worst case certain situations which have the potential to reduce safety levels may be missed.

The PhD study will develop such theories for modelling and verifying complex networks comprising areas with mixed signalling. The general aim is to come up with a general, open and extendable agent-based framework to enable capturing any type of signalling, legacy or new, and to assist signalling engineers in ensuring safety of such heterogeneous systems.

The theories will provide a formal foundation for fully automated verification of system safety that can be tool supported with the use of the advanced mechanised theorem proving.
As an important part of the study we will also develop techniques to support evaluation of heterogeneous systems' capacity.

The study will focus on supporting the application of such theories by a set of tools that have domain-specific interfaces and are scalable and useable.

The work will be driven by the needs of industry and conducted in a close cooperation with Siemens Rail Automation (Chippenham) to ensure that the results have potential to be deployed in real industrial settings.

Studentship Projects

Project Reference Relationship Related To Start End Student Name
EP/N509528/1 01/10/2016 30/09/2021
1798533 Studentship EP/N509528/1 01/10/2016 30/12/2020 Paulius Stankaitis
 
Description Over the last few decades, developments in communication and computing technologies have enabled railway engineers to develop novel railway signalling systems. The modern railway signalling systems, such as European Train Control System (ETCS) or Communication-Based Train Control (CBTC) are safety-critical cyber-physical transportation systems which should increase railway network capacity, interoperability and reliability. However, modernisation process requires a lot of resources, so, this process will be gradual, thus creating heterogeneous railway signalling networks. In other cases, mainline network will be integrated with urban networks (e.g Crossrail Network, London) creating another type of heterogeneous signalling system. The rolling stock must transition from one signalling network to another with the heterogeneous signalling system ensuring safe and on the fly transition.

In this work we addressed the issue of formal modelling and verification of the heterogeneous railway signalling systems. The key finding and outcomes of this research are summarised below:

- A formal methodology for engineering heterogeneous railway signalling systems
- Modelling patterns and templates for modelling railway systems
- Improved verification automation of formal models
Exploitation Route The methodology we proposed and developed integrated different state-of-the-art tools. The method, however, could highly benefit from a seamless model translation between different tools, which is currently not supported.
Sectors Digital/Communication/Information Technologies (including Software),Transport

 
Description Collaboration with ENSEEIHT (Toulouse, France) and NII (National Institute of Informatics) 
Organisation ENSEEIHT
Country France 
Sector Academic/University 
PI Contribution I have been leading these collaborations and was primarily responsible for conducting research and writing papers.
Collaborator Contribution - The partners of these collaborations have provided domain expertise and help in developing new formal techniques for a hybrid system development. - The partners of these collaborations have also provided an office and covered a part of travelling expenses when I was visiting their departments.
Impact The main outcomes of these collaborations have publications (3 papers) and improvements to the software tool used for model verification.
Start Year 2017
 
Description Collaboration with ENSEEIHT (Toulouse, France) and NII (National Institute of Informatics) 
Organisation National Institute of Informatics (NII)
Country Japan 
Sector Public 
PI Contribution I have been leading these collaborations and was primarily responsible for conducting research and writing papers.
Collaborator Contribution - The partners of these collaborations have provided domain expertise and help in developing new formal techniques for a hybrid system development. - The partners of these collaborations have also provided an office and covered a part of travelling expenses when I was visiting their departments.
Impact The main outcomes of these collaborations have publications (3 papers) and improvements to the software tool used for model verification.
Start Year 2017
 
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
 
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 Exhibiting the SafeCap tool at the industrial conference 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach National
Primary Audience Industry/Business
Results and Impact We had a stand at the SIG X-20 event organised by Network Rail in February 2020 in Bristol. Our aim was to demo the SafeCap toolset and to engage with the companies that could use it.
Year(s) Of Engagement Activity 2020
 
Description Tutorial on using SafeCap for signalling verification 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Professional Practitioners
Results and Impact Tutorial entitled SafeCap: Automated formal verification of railway signalling interlockings was given at the RSSRail 2019 conference in Lille. RSSRail is a unique conference focusing on advancing the cooperation between academia and industry. The tutorial was well received with many followup discussions and new cooperations established.
Year(s) Of Engagement Activity 2019
URL https://conferences.ncl.ac.uk/rssrail2019/tutorials/