Holistic Study of Formal Methods and Standardization in Specification, Development, Verification and Validation of Railway Signalling System Software

Abstract

Tender requirements for rail control tend to be vague and imprecise, demanding significant effort and know-how to be interpreted and detailed. This leads to critical design choices whose impact is not understood until late phases. Verification is mainly based on manual review and test, that do not provide assurance that critical system properties always hold. Reuse is limited, due to lack of standardized system architecture and interfaces, resulting in wasted effort from project to project, and the need to manage and maintain several system variants. These root causes make schedules to deliver systems long and unpredictable, and systems costly to procure, develop and maintain. Shift2Rail technology demonstrator TD2.7 studies how formal methods (FMs) and standardization help address these root causes. This article describes two complementary case studies, together with a business case perspective, for FMs use in specification, development and verification and validation (V&V) of rail control software. What is new in this work is that industry practitioners and researchers in Shift2Rail collaborated to define a taxonomy of FM use cases for rail control and applied them to real-world subsystems. Together, this holistic study combines all those FMs use cases and many individual FMs and tools considered state-of-the-art to demonstrate that using FMs is feasible and worthwhile.