A New Formal Methods Guidebook for the Railway Signalling Domain

Abstract

Considerable know-how about formals methods (FMs) exists in the railway signalling domain, and FMs have been successfully applied e.g. for verification of interlockings or development of computer-based train control systems. But FMs expertise is not generally available or widespread, and there is a lack of FMs integration into standards, of recommendations for FMs use and of guidance on where and how to employ them. For these reasons, TD2.7 of Shift2Rail is currently preparing a FMs guidebook which aims to document know-how, experience, and recommendations, to pave the way for wider use of FMs for today's and future railway signalling systems. In this contribution, the guidebook contents are briefly presented, including why, when and for what purpose to apply FMs, what FMs are and which steps their application follows. Afterwards, an example application of the guidebook's FMs concepts is described.