Models for formal methods and tools: the case of railway systems

Formal methods and tools are successfully applied to the development of safety-critical systems for decades now, in particular in the transport domain, without a single technique or tool emerging as the dominant solution for system design. Formal methods are highly recommended by the existing safety standards in the railway industry, but railway engineers typically lack the knowledge to transform their semi-formal models into a formal model, with a precise semantics, that can serve as input to formal methods tools. We share the results of performing empirical studies in the field, including usability analyses of formal methods tools involving railway practitioners. We discuss, in particular with respect to railway systems and their modelling, our experiences in applying formal methods and tools to a variety of case studies, for which we interacted with a number of companies from the railway domain. We report on lessons learned from these experiences and provide pointers to steer future research towards facilitating further synergies between researchers and developers of formal methods and tools on the one hand and practitioners from the railway industry on the other.