A Verification-Aware Pipeline for Programmable Logic Controllers: From Function Block Diagrams to Verified Python Code

Translating programmable logic controller (PLC) programs into analyzable software artifacts is an important step toward enabling modern software testing and verification techniques in industrial settings. This paper presents a replication study in which we use PyLC+, a translation framework for IEC 61131-3 Function Block Diagrams (FBD), together with the Nagini verifier to perform functional correctness checks on industrial safety-critical logic. PyLC+ extracts block networks from PLCopen XML and generates executable Python models that preserve block semantics, signal flow, and scan-cycle behavior. We applied this workflow to a representative set of 13 industrial POUs from an electropneumatic brake control subsystem. All 13 POUs were verified: twelve using concrete or partially abstracted FBD models, and one using an abstract requirements-level specification whose 7-tuple specification initially exposed a bug in the Nagini verifier (a lack of support for tuples with more than six elements), which was fixed by the Nagini developers. The results show that a combination of automated extraction, manual semantic reconstruction, and contract-based specification is sufficient to verify realistic industrial logic at the POU level. We also discuss the abstraction decisions, the Nagini bug uncovered by one POU, and the remaining missing block semantics that constrain how far automation can be pushed in future versions of PyLC+.