Group Overview
The Swansea Railway Verification Group was founded in 2007. Its purpose initially was to explore multidisciplinary problems between formal methods, management of new technologies, and rail engineering posed by Invensys Rail (now Siemens Rail UK), a multinational technology leader, providing state-of-the-art software-based signalling, communication and control systems that enable the safe and efficient operation of trains in mainline and mass transit networks across the world. Whilst this is still its main focus, its reach and impact have been expanded with projects funded by EPSRC and RSSB.
The Group works with similar groups in computer science, engineering, and management throughout the UK, Europe, and in China. Since 2015 SRVG has led on the European Technical Working Group on Formal Methods in Railway Control (chaired by MR). In 2017, MR was appointed International Committee Advisor for the International Joint Research Center for Rail Traffic Control and Safety, a joint venture of the State Key Lab of Traffic Control and Safety, China, and Jiatong University China; for the academic year 2018/19, Mr Yong Zhang from the National Engineering Research Center of Rail Transportation Operation and Control System, Beijing Jiaotong University, Beijing, China, has joined SRVG as a visiting research student.
In 2004, the 18th IFIP World Computer Congress identified the railway domain as a Grand Challenge of Computing Science because it is of immediate concern and because it also provides a set of generic, well-understood problems whose solutions would be transferable to various other application domains, e.g., process control in manufacturing, also known as industry 4.0. In this context, the SRVG carries our multidisciplinary research concerning formal safety guarantees, the usability of verification methods in railway engineering, and the economic case for adopting formal methods in industry. This concerns the design of various artefacts central to industrial rail control software, including Ladder Logic Programs, Control Tables, Release Tables, RBC Tables.
In co-creation mostly with Siemens Rail UK, but also reaching out, e.g., to State Railway of Thailand, SRVG works on challenges of various nature: how to develop faithful and traceable models of railway designs (there is an established Swansea railway modelling approach); how to circumvent the state space explosion problem with suitable abstractions and compositional verification methods proven to be sound; how to automate verification approaches and encapsulate them in tools; how to interface between industrial and academic tools; how to empirically demonstrate and measure the benefits of utilizing Formal Methods. Over the last decade, SRVG made a number of respected contributions to all these areas – see the below list of publications. In terms of technology readiness levels, the work of SRVG encompasses the full spectrum from TRL 1 – basic principles observed – to TRL 5 – technology validated in an industrially relevant environment. To this end, scientists from Swansea University have extensively studied and continue to study the field of railway engineering, whilst Siemens rail engineers have been exposed are continue to be exposed to various forms of formal modelling and verification techniques. Reaching out to experts in the management of new technologies, e.g., from the Leeds Institute for Transport Studies, Swansea scientists and Siemens engineers are currently widening the scope of their collaboration by including economic appraisal techniques. Only thanks to such interdisciplinary knowledge exchange, the successes as mentioned above are possible.
Current research focuses on developing, verifying, and formal testing from hybrid models for safety verification of the European Rail Traffic Management System (ERTMS); and on an empirical software engineering review and economic appraisal for the use of automated verification techniques when designing Ladder Logic programs for interlockings. For the former, SRVG holds an iCASE PhD studentship with Siemens. For the latter, SRVG led by P James collaborates with Siemens rail engineers on the research project “Ladder Logic Verification”. As part of this new initiative, Siemen Rail is now committing software engineers to the task of embedding bespoke versions of SRVG verification tools into their design process.
