Interlocking Formal Verification at Alstom Signalling

摘要

Over the past decade, the growing number of safety-critical software in the railway signalling industry has led customers and industrials to look for efficient, cost-effective, verification and validation techniques. Formal methods, which have proven to be applicable and beneficial in terms of accuracy and completeness, are good candidates. However, they are still far from being used systematically for the verification of all safety-critical railway signalling systems. In order to evaluate their applicability, Alstom successfully experimented on its interlocking systems the model checking methods and tools developed by Systerel. This article describes the methodology used to industrialize this experimental model checking application process.