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.

The Centre will nurture 55 new PhD researchers who will be highly sought after in technology companies and application sectors where data and intelligence based systems are being developed and deployed. We expect that our graduates will be nationally in demand for two reasons: firstly, their training occurs in a vibrant and unique environment exposing them to challenging domains and contexts (that provide stretch, ambition and adventure to their projects and capabilities); and, secondly, because of the particular emphasis the Centre will put on people-first approaches. As one of the Google AI leads, Fei-Fei Li, recently put it, "We also want to make technology that makes humans' lives better, our world safer, our lives more productive and better. All this requires a layer of human-level communication and collaboration" [1]. We also expect substantial and attractive opportunities for the CDT's graduates to establish their careers in the Internet Coast region (Swansea Bay City Deal) and Wales. This demand will dovetail well with the lifetime of the Centre and provide momentum for its continuation after the initial EPSRC investment.

With the skills being honed in the Centre, the UK will gain a important competitive advantage which will be a strong talent based-pull, drawing in industrial investment to the UK as the recognition of and demand for human-centred interactions and collaborations with data and intelligence multiplies. Further, those graduates who wish to develop their careers in the academy will be a distinct and needed complement to the likely increased UK community of researchers in AI and big data, bringing both an ability to lead insights and innovation in core computer science (e.g., in HCI or formal methods) allied to talents to shape and challenge their research agenda through a lens that is human-centred and that involves cross-disciplinarity and co-creation.

The PhD training will be the responsibility of a team which includes research leaders in the application of big data and AI in important UK growth sectors - from health and well being to smart manufacturing - that will help the nation achieve a positive and productive economy. Our graduates will tackle impactful challenges during their training and be ready to contribute to nationally important areas from the moment they begin the next steps of their careers. Impact will be further embedded in the training programme with cohorts involved in projects that directly involve communities and stakeholders within our rich innovation ecology in Swansea and the Bay region who will co-create research and participate in deployments, trials and evaluations.

The Centre will also impact by providing evidence of and methods for integrating human-centred approaches within areas of computational science and engineering that have yet to fully exploit their value: for example, while process modelling and verification might seem much removed from the human interface, we will adapt and apply methods from human-computer interaction, one of our Centre's strengths, to develop research questions, prototyping apparatus and evaluations for such specialisms. These valuable new methodologies, embodied in our graduates, will impact on the processes adopted by a wide range of organisations we engage with and who our graduates join.

Finally, as our work is fully focused on putting the human first in big data and intelligent systems contexts, we expect to make a positive contribution to society's understandings of and involvement with these keystone technologies. We hope to reassure, encourage and empower our fellow citizens, and those globally, that in a world of "smart" technology, the most important ingredient is the human experience in all its smartness, glory, despair, joy and even mundanity.

[1] https://www.technologyreview.com/s/609060/put-humans-at-the-center-of-ai/