A Survey on Formal Methods for Railway Interlockings: From Relays to Satellite-Based Moving Block Signaling

An interlocking constitutes an arrangement of railway signaling equipment with the aim to guarantee the safe movement of trains. A wide range of formal methods have been applied in the analysis of interlockings, often in close collaboration with industry. Moreover, different formal frameworks and techniques have been developed that target the efficient analysis of interlockings and the integration of such mathematically rigorous methods into industrial design processes. This survey provides a comprehensive overview of this field, including a wide variety of case studies, ranging from relay-based interlocking systems to recent developments regarding satellite-based moving block technologies. It is also explained how computer-based interlockings for different railway yards can be developed in a uniform, object-oriented fashion, based on their track layouts. Furthermore, an overview is given of domain-specific languages for developing and analyzing interlockings using formal methods and tools in an industrial setting. The main aim is to fit the wide range of papers in this research area into coherent narratives, showing how the employment of formal methods to interlockings has progressed in the last decades. This survey concludes with discussing research gaps and important directions for future research.