Survey on Formal Methods and Tools in Railways Technical Report on the activities performed within ASTRail, Deliverable D4.1

Formal methods have been largely experimented in industry for the development of safety-critical and mission critical products. Despite the quite long story of successful application of formal methods in the railway domain, it cannot yet be said that a single mature technology has emerged. Indeed, any proposed method or technique that goes under the umbrella of formal methods varies in its suitability and applicability to different stages of the signalling system development, and to different subdomains of railway signalling. This Work Package 4 of the ASTRail project aims to identify, on the basis of an analysis of the state of the art, of the past experiences of the involved partners and on work done in previous projects, the candidate set of formal and semi-formal techniques that appear as the most adequate to be used in the different phases of the conception, design and development of a railway equipment in general, and of the class of signalling equipment that is the subject of this project in particular. To this end, we perform a survey that considers scientific literature, international projects, and practitioners’ perspectives to identify a collection of formal methods and tools to be applied in railways. This technical report summarises the current results of this WP. We surveyed 114 scientific publications, 44 practitioners, and 8 projects to come to a shortlist of 14 methods considered suitable for system modelling and verification in railways. The methods and tools were reviewed according to a set of functional, language-related, and quality features. The current paper extends the body of knowledge with a set of publicly available documents that can be leveraged by companies for guidance on formal methods selection in railway system development