Can machine learning approaches be applied to automated invariant finding during verification of ladder logic program

点击翻译按钮获取中文摘要

Industrial standards for the railway and related domains are increasingly relying 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. In a cross-disciplinary avenue involving experts from both engineering and computer science, this project sets out to co-create such an impact in an academic-industry partnership between Siemens Rail Automation UK and academics with specialisms in formal methods and machine learning at Swansea University. This impact will be evidenced by demonstrating the benefits of applying machine learning to aid an existing formal based design processes of so-called interlocking systems.An interlocking system is responsible for guiding trains safely through a given railway network. It is a vital part of any railway signalling system and has the highest safety integrity level (SIL4) according to the CENELEC 50128 standard. Interlockings run software commonly written in Ladder Logic, a graphical language encoding Boolean expressions.In this project, we will utilise verification approaches for Ladder Logic developed across several projects carried out at Swansea University (see http://cs.swansea.ac.uk/Rail) in co-operation with Siemens Rail Automation UK. We will aim to explore if approaches within machine learning [13, 14] can be used to improve the efficiency of verification whilst also reducing the number of false positives that are reported by the current approach.