4 papers · 1 filter
K-ESBMC: An Executable Formal Semantics of IEC 61131-3 Ladder Diagram for Validating Verifier Translations
Pierre Dantas, Lucas Cordeiro, Waldir Junior
Automated verifiers for IEC 61131-3 ladder diagrams enhance safety by translating diagrams into model-checker inputs. Still, their unverified front-end translations risk silently r…
ESBMC-Arduino: Closing the Deployment Gap for Formal Verification of Open-Hardware PLCs
Pierre Dantas, Lucas Cordeiro, Waldir Junior
OpenPLC, Arduino OPTA, CONTROLLINO, and Industrial Shields M-Duino bring IEC 61131-3 to low-cost microcontrollers used in real automation and industrial control system (ICS) securi…
ESBMC-PLC+: A Unified IEC 61131-3 Formal Verification Framework as a PLCverif Successor
Pierre Dantas, Lucas Cordeiro, Waldir Junior
PLCverif is the most mature open-source platform for PLC formal verification, developed at CERN and in production use since 2019. Yet it has two fundamental limitations: no support…
ESBMC-GraphPLC: Formal Verification of Graphical PLCopen XML Ladder Diagram Programs Using SMT-Based Model Checking
Pierre Dantas, Lucas Cordeiro, Waldir Junior
PLCopen XML defines two encoding formats for IEC 61131-3 Ladder Diagram programs: a textual encoding using <rung> elements, and a graphical encoding that represents rung logic as a…