Swansea Railway Verification Group
In 2007, Professor Faron Moller started a collaboration with Invensys Rail, a multinational technology leader based in Chippenham, which provides state-of-the-art signalling, communication and control systems for mainline and mass transit rail networks across the world. The success of this collaboration resulted in the creation of the Swansea Railway Verification Group, generously supported by Invensys Rail as well as the RSSB (Rail Safety and Standards Board) and EPSRC. In particular, Invensys Rail has provided full or partial funding (thus far) for three MRes students, three PhD students and seven summer research students working on problems of interest to the company. These projects include SAT-based verification and model-checking of interlocking; combining radio block processors and interlockings; developing domain-specific languages for interlocking; and overcoming railway capacity. In the following we highlight some of the major activities of the Group.
Research carried out by the group is having impact on both current practices and strategic planning within the railway industry. Regarding current practices, research led by Professor Moller, Dr Monika Seisenberger and Dr Anton Setzer has resulted in the adoption of formal verification techniques within the interlocking design stage at Invensys Rail. Regarding strategic planning, research led by Professor Moller and Dr Markus Roggenbach is addressing the problem of the adoption of ETMS (Electronic Train Management System) by the UK as a replacement for traditional track-side interlocking. ETMS, which uses GPS for positioning and a digital radio system to monitor train location and speed, is being introduced throughout Europe as part of ERTMS (the European Rail Traffic Management System), but UK train companies are resisting this change due to the high cost of entry (replacing and equipping rolling stock). Our research here – which is in part funded by the RSSB – is producing data for the use of RSSB and the network operators to convince train operators – and government – of the need to invest in change.
Overcoming the constraints on railway capacity caused by nodes (stations and junctions) on the rail network is one of the most pressing challenges to the rail industry. In 2007, the UK governmental White Paper‚ Delivering a Sustainable Railway‚ stated: “Rail’s biggest contribution to tackling global warming comes from increasing its capacity.” High capacity, however, is but one design aim within the railway domain. Railways are safety-critical systems. Their malfunction could lead to death or serious injury to people, loss or severe damage to equipment, or environmental harm.
Within the SafeCap project, Dr Roggenbach, Professor Moller, and Dr Hoang Nga Nguyen develop formal models of railway nodes, prove that they are safe, and investigate how to measure and how to improve their capacity. This work is carried out in close cooperation with Invensys Rail as the industrial partner, Professor Alexander Romanovsky (Newcastle University), and Dr Yoshinao Isobe (AIST, Japan). Research on tool support for specification languages includes the development of CSP-Prover, an interactive theorem prover for the process algebra CSP, and tools for Timed CSP, such as a Timed CSP-Simulator.
Also in the context of railways, Dr Roggenbach studies the formalization of Domain Specific Languages (DSLs) within the algebraic specification language CASL to ease system verification. By systematically capturing domain specific knowledge, and then tailoring proof goals around this domain specific knowledge, one can improve automatic verification results, whilst also providing a graphical domain specific language. This process builds upon the common industrial practice to describe the domain specific vocabulary in terms of DSLs.