Summary of the impact

The UK Rail Industry has set itself a target of increasing capacity by a factor of two within 30 years for both passengers and freight. A central problem is to increase the capacity and performance of the (existing) rail network. Signalling systems and their safety is a major consideration. It is towards this long-term goal that we direct our research activity on signalling. Our research impacts both current practices and strategic planning within the Railway Industry:

• Current practices: Our research has led to (i) the adoption of formal verification techniques at Invensys Rail, a multi-national technology leader, as well as (ii) changes in the operation and organisation of the company - involving personnel, structures and forward thinking - that successfully address commercial challenges faced by the company.
• Strategic planning: The adoption of the European Train Management System (ETMS) - a proposed replacement for track-side signalling - is aimed at reducing maintenance costs, enhancing performance and improving safety. But its adoption presents a major challenge for the UK. In addressing this, our research produces data and thinking in support of change, which we deliver through various working groups and initiatives that are developing national policy for the development of the UK railway. By releasing UK railways from the strictures of track-side signalling, ETMS represents the step-change transformation necessary for meeting the industry's ambitious 30-year target.

Underpinning research

Traditional track-side signalling represents a major constraint for the UK Railway industry. It requires a route to be free of - i.e., not in any part reserved for - any rail traffic before any of the signals (traffic lights) along the route are set to allow the movement of a train along the route. This is the essence of the railway interlocking problem. In this setting, rail companies are faced with the commercial challenge of designing interlocking hardware and software which guarantees that trains run efficiently whilst above all safely. Around the world, contracts worth billions of dollars are up for tender; and the UK Rail industry itself is being faced with the challenge of meeting vocal public demand for increased capacity on railway traffic.

Swansea University has a long history of internationally excellent research and researchers working on the wide variety of semantic models, formal design methods and software tools that are of direct relevance to the needs of railway signalling design: model checking, constraint solving, type theory, theorem proving, software specification, and (especially) process algebra. Indeed, while a lecturer in Computer Science at Swansea, Professor Wan Fokkink (now at Free University, Amsterdam) wrote a research monograph titled LARIS1.0: Language for Railway Interlocking Specifications (CWI Publications, 2000). This monograph was contracted by Nederlandse Spoorwegen (Dutch Railways) and was based on a process algebra formalism.

The underpinning research for the impact described began with an initial period of consultation in 2007 between Prof Faron Moller, Swansea University and the Vice President (Technology) - now Senior VP (Engineering) - of Invensys Rail. This consultation was initially concerned with research and development relevant to a specific high-value contract for underground railway signalling secured by the company. Based on the success of this consultation, Invensys Rail agreed to financially support two research students at Swansea (subsequently Dr K Kanso and Dr P James) to develop theoretical and practical tools to aid in the design of railway interlocking systems relevant to the contract. Our research here [Publications R1, R2] was applied to case studies based on actual underground stations and terminals.

Building on the success of this effort, the collaboration expanded into laying out the railway problem domain in the context of employing formal technologies and identifying ways in which Invensys Rail could develop an industrial research programme. This led to a re-organisation in the company involving the appointment of a Director of Research, and to Invensys Rail offering full or partial funding for: three MRes students; three PhD students; and seven summer research students working in the Department on problems of interest and relevance 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 [R3]; and novel approaches to overcoming railway capacity [R4-6].

References to the research

Publications (the latter three, [4,5,6], best indicate the quality of the underpinning research); Swansea authors in bold

Grants and Contracts

G1.RSSB/EPSRC Project EP/I010807/1, SafeCap: Overcoming the railway capacity challenges without undermining rail network safety. EPSRC Reference EP/I010807/1, £451,190 (full economic cost). February 2011 - July 2013. (This was a joint grant with Newcastle University, though with each institute following independent research programmes; the sum above is that generated by Swansea University, the grant holder being Dr Markus Roggenbach.)

G2.Invensys Rail Project, Railway Control Systems. £103,500. October 2008 - December 2014. (Grant holder Faron Moller.)

G3.Swansea holds a Joint Research Contract with the AIST Japan, which includes cooperation on railway research. (The contract provides no direct costs to Swansea University, but supports bilateral visits funded by the Japanese Institute.)

Details of the impact

At the end of this section we bullet-point our specific research contributions; before that we outline their development and in so doing demonstrate their authenticity.

The Swansea Railway Verification Group [C1], supported by eight academics, is a direct result of the research underpinning the impact. Its various projects are motivated by interactions with Invensys Rail, a company with a powerful heritage in the railway industry stretching back 140 years. Since 1935 Invensys has had its head office in Chippenham, and it currently employs over 4,000 people worldwide within the Invensys group of companies which together have over 20,000 employees. (On 2 May 2013 Invensys Rail was acquired by Siemens but continues to operate under the name Invensys Rail as part of Siemens' Rail Automation Business Unit.)

With a growing track record in rail signalling research, the Swansea Railway Verification Group was awarded an EPSRC Grant entitled SafeCap [C2] worth £450,000 (full economic costing) to Swansea University which supports one full-time PDRA and part of the time of Faron Moller and Dr Markus Roggenbach. While administered by EPSRC, this grant is in fact funded by the Rail Safety and Standards Board (RSSB) and was awarded after an open call and extensive review process by RSSB with a full interview stage. The call was for research ideas that would have the greatest potential for impact on overcoming capacity constraints on railways; SafeCap was ranked second of five successful proposals [C3]; and its success has led to the Group being invited to contribute to the development of an Academic Research Strategy Document impacting on strategic decisions in policy making at national level.

According to the Senior VP (Engineering) for Invensys Rail [C4], "the Swansea Railway Verification Group can be said to have had an impact on changing attitudes and practices at head office level within Invensys Rail, a long-established multi-national company." Evidence of this impact provided by this Senior VP is outlined below.

In 2007 the Senior VP (Engineering) was VP (Technology) at Invensys. As he describes in his letter, he invited Moller to Chippenham to consult on a major project on which the company was working; this multi-million-pound contract involved developing software for controlling interlockings at 111 stations in the UK, and he sought expert advice from Moller about what theoretical and formal methods tools were available, or could be developed, to stream-line this mammoth task.

With this initial consultation, the VP (Technology) embarked on developing a research-focussed ethos in the company and welcomed Moller's input on this vision. The creation of the Swansea Railway Verification Group, with its many projects supported by Invensys Rail, attests to this vision. Apart from the VP (Technology), three further members of staff at Invensys Rail have been directly involved in this research and contributed large amounts of time and effort to it: the Director of Research (a new post created early on in the research programme); and two Senior Solutions Architects. According to the VP (Technology), "it is a direct consequence of the engagement with the Swansea Railway Verification Group that the new position of Director of Research was created in the company." Various other members of the technical staff at the company have also engaged with the different projects at various times in order to ensure that the research being carried out can be effectively deployed in practice.

According to the Director of Research at Invensys [C5], "the research carried out in Swansea - in particular the verification tools developed - has directly led to the adoption of formal verification tools and techniques within the interlocking design stage. The company's motivation with this is to cut down greatly on the time taken to deliver interlocking systems by reducing the expensive and time-consuming testing cycle inherent in the process. With these techniques in place, many design problems can be identified and rectified at the design stage before going into the testing phase." Also according to the Director of Research, "we have engaged with you on a variety of discussions exploring various regulatory and commercial necessities, and explored with you a wide spectrum of formal methods technologies on live problems emanating from ongoing Invensys Rail contracts."

Specific Research Contributions and their Impacts

Specific research contributions providing impact are as follows:

• The adoption of formal verification techniques within the interlocking design stage at Invensys Rail.
• The development of a novel modelling language and approach to modelling systems with which technical staff within the railway industry can build models in a way which is natural to their engineering understanding; they are no longer hindered by the use of traditional solid state interlocking languages, nor by the unnatural and incomprehensible nature of the alternatives proposed by the research community.
• The analysis of performance data which examines line and network capacity constraints, with a view to identifying means for improving capacity on the UK railway network under the existing traditional interlocking technology.
• The analysis of the strategic merits of adopting ETMS, both alongside and in place of existing interlocking systems.

Our impact reaches beyond Invensys Rail into national regulatory bodies. According to a Principle Engineer at Network Rail [C6], "the impact of the SafeCap project is that it has changed attitudes at Network Rail by demonstrating the potential and the benefits of Formal Methods to Railway design. The SafeCap results promise to reshape the GRIP design process for early stage safety and capacity analysis." (GRIP stands for Governance for Railway Investment Projects and is the standard employed at Network Rail for managing and controlling projects; compliance to the standard is mandatory, so influence on the shape of GRIP represents substantial impact on Network Rail practices.)

Due to the success of our research efforts, we

• contributed to a paper solicited by the Institute of Railway Signal Engineers (IRSE) entitled "The Future of Train Control Systems" which was presented and discussed by railway signal engineers at their meeting in London on 13 February 2013, and later presented by invitation to the Rail Accident Investigation Branch (RAIB) on 14 May 2013. [C7]
• were invited to join a panel to develop an Academic Research Strategy Document as a response to the Rail Transit Strategy 2012, which seeks "a national policy for the development of the railway over a 30-year planning horizon." [C8]
• have the credibility to lead on the first compilation of a Body Of Knowledge in Formal Methods in Rail, to be developed from a Workshop titled FM-RAIL-BOK that we will organise in September 2013. The committee overseeing this Workshop includes various representatives from industry and rail standards boards. [C9]

Sources to corroborate the impact

C1.Swansea Railway Verification Group website www.cs.swan.ac.uk/Rail

C2. SafeCap Project website safecap.cs.ncl.ac.uk/index.php/Saefcap_Project_Wiki

C3. RSSB Website listing SafeCap as one of five successful bids (ranked second) to their call on capacity www.rssb.co.uk/RESEARCH/cofunding/Pages/StrategicEPSRCClosed.aspx

C4. Letter from the Senior Vice President (Engineering), Invensys Rail.

C5. Letter from the Director of Research, Invensys Rail.

C6. Letter from a Principal Engineer, Network Rail.

C7. IRSE Technical Paper, "The Future of Train Control Systems".

C8. Academic Research Strategy Document rruka.org.uk/a-meeting-of-the-minds

C9. FM-RAIL-BOK Workshop 2013 website ssfmgroup.wordpress.com