The speaker for next week’s theory seminar will be our own Markus (see title and abstract below). We will meet next Tuesday (Oct 20) at 2pm in the theory lab.

Title

Verifying Ladder Logic Programs Theory and Practice

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.