Title:
Can machine learning be applied to automated invariant finding during verification?
External Stakeholder:
Siemens Rail Automation UK.
The Research:
Solid state interlockings are computerised systems responsible for ensuring safe routing of trains through a given bounded network. As a vital part of any railway signalling system, interlockings are critical systems regarded with the highest safety integrity level (SIL4) according to the CENELEC 50128 standard. The application of model checking to Ladder Logic programs in order to verify interlockings is well established within academia and is beginning to see real applications in industry. As early as 1995, Groote et al. applied formal methods to verify an interlocking for controlling the Hoorn-Kersenbooger railway station. They conjecture the feasibility of verification techniques as means of ensuring correctness criteria on larger railway yards. In 1998, Fokkinkand Hollingshead suggested a systematic translation of Ladder Logic into Boolean formulae. Newer approaches to interlocking verification have also been proposed in recent years. This includes work by Linhet al. which explores the verification of interlockings written in a similar language to Ladder Logic using SAT-based model checking. After two decades of research, academic work has shown that verification approaches for Ladder Logic can indeed scale; in an industrial pilot Duggan et al. conclude: “Formal proof as a means to verify safety has matured to the point where it can be applied for any railway interlocking system.” In spite of this such approaches still lack widespread use within the UK Rail industry. The primary goals of this PhD are to address two issues hindering such uptake; firstly by addressing the longest loop free path problem for bounded model checking, and second attempting remove the need for manual analysis of false negative errors during verification.
Industrial standards for the railway and related domains increasingly rely on the application of formal methods for system analysis in order to establish a design’s correctness and robustness. Recent examples include the 2011 version of the CENELEC standard on railway applications, the 2011 ISO 26262 automotive standard and the 2012 Formal Methods Supplement to the DO-178C standard for airborne systems. However the application of formal methods research within the UK rail industry has yet to make a substantial impact. This interdisciplinary project strives to establish new theoretical and practical frameworks in an academic industry partnership with Siemens Rail Automation UK. Primarily, we aim to demonstrate the benefits of applying machine learning to aid the existing design processes for railway interlocking systems.