Towards integrated simulation and formal verification of rail yard designs - an experience report based on the UK East Coast Main Line

The development of railway systems is often supported by a range of tools, each addressing individual, but overlapping concerns such as, e.g., performance or safety analysis. However, it is a challenge for users to organise work-flows; results are often in different, non-aligning data formats; furthermore, tools work on different levels of abstraction from macro to microscopic. Thus, tool integration would be beneficial, and also allow for more playful, experimental prototyping and design. This paper reports on lessons learned from the integration of BRaVE - the Birmingham Railway Virtual Environment - and OnTrack from Swansea University. BRaVE is an easy-to-use railway simulation software for development, modelling and flow analysis. OnTrack allows for the automatic verification of scheme plans against a number of safety properties via different formal methods. We present an approach that bridges the gap that occurs from varying details in data sources through automated transformations. This integration provides a first step towards a seamless environment for prototyping, concept development, and safety analysis under ”one roof”. We demonstrate the usefulness of our approach by giving integrated simulation and verification results for the UK East Coast Main Line. This work is part of the wider RSSB's Future Traffic Regulation Optimisation research programme.