Verifying Ladder Logic Programs in the Railway Domain – Theory and Practice
Markus Roggenbach
Swansea University, United Kingdom
ABSTRACT
Programmable Logic Controllers (PLCs) are used within many applications across various industries: examples include monitoring solar cells, robot control (spraying toxic chemical substances; washing the face glasses of skyscrapers), packaging and labelling systems, nuclear power plants, railway control systems.
The International Electrotechnical Commission specifies syntax and semantics of programming languages for such programmable controllers in its standard IEC 61131, part 3. This standard covers the graphical language “Ladder Diagrams”, often also called Ladder Logic. According to a 2022 article in the journal “Manufacturing Tomorrow”, “Ladder Logic is the main programming method used for PLCs”.
The invited talk will cover how to provide a formal semantics to Ladder Logic programs running on a PLC, how to define a logic expressing safety properties, and discuss various methods for verifying that a program is safe, including the IC3 algorithm. It turns out that software model checking of real-world programs is feasible, i.e., Ladder Logic verification provides a success story where a Formal Methods scales to industrial needs. Verification examples from the railway domain will illustrate the approach.
SHORT BIO
Markus Roggenbach is a Professor of Computer Science at Swansea University, UK. There, he leads the interdisciplinary Swansea Centre for Research in Digital Railways as well as the Cyber Security Group in the Department of Computer Science. His research foci are formal methods for safety and for cyber security, their semantics, how to utilise them throughout the software life cycle, how to support them with tools, and their application in industrial contexts, e.g., the railway domain. He is a member of the Federation for Information Processing (IFIP) Working Group 1.3 “Foundations of System Specification” (chair in 2015 – 2021). Markus has co-authored the book “Formal Methods for Software Engineering”, Springer, 2022.