On Formal Reasoning on the Semantics of PLC using Coq

Understand

Programmable Logic Controllers (PLC) and its programming standard IEC 61131-3 are widely used in embedded systems for the industrial automation domain.

• We propose a framework for the formal treatment of PLC based on the IEC 61131-3 standard.
• A PLC system description typically combines code written in different languages that are defined in IEC 61131-3.
• For the top-level specification we regard the Sequential Function Charts (SFC) language, a graphical high-level language that allows to describe the main control-flow of the system.