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

铁路和相关领域的工业标准越来越依赖于系统分析的形式化方法的应用，以建立设计的正确性和鲁棒性。最近的例子包括：2011年版的铁路应用CENELEC标准；2011年ISO 26262汽车标准；以及2012年航空系统DO-178C标准的正式方法补充。然而，正式方法研究在英国铁路行业的应用尚未产生实质性影响。在涉及工程和计算机科学专家的跨学科途径中，该项目旨在共同创造西门子铁路自动化英国公司与斯旺西大学正规方法和机器学习专业学者之间的学术-行业合作伙伴关系的影响。这种影响将通过展示应用机器学习来帮助现有的基于正式的所谓联锁系统设计过程的好处来证明。联锁系统负责引导列车安全通过给定的铁路网。它是任何铁路信号系统的重要组成部分，根据CENELEC 50128标准具有最高的安全完整性等级（SIL4）。联锁运行的软件通常用梯形逻辑（一种编码布尔表达式的图形语言）编写。在这个项目中，我们将利用在斯旺西大学（见http://cs.swansea.ac.uk/Rail）与西门子铁路自动化英国公司合作开展的几个项目中开发的梯子逻辑的验证方法。我们的目标是探索机器学习中的方法[13,14]是否可以用于提高验证效率，同时减少当前方法报告的误报数量。

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.