You are required to read and agree to the below before accessing a full-text version of an article in the IDE article repository.

The full-text document you are about to access is subject to national and international copyright laws. In most cases (but not necessarily all) the consequence is that personal use is allowed given that the copyright owner is duly acknowledged and respected. All other use (typically) require an explicit permission (often in writing) by the copyright owner.

For the reports in this repository we specifically note that

  • the use of articles under IEEE copyright is governed by the IEEE copyright policy (available at http://www.ieee.org/web/publications/rights/copyrightpolicy.html)
  • the use of articles under ACM copyright is governed by the ACM copyright policy (available at http://www.acm.org/pubs/copyright_policy/)
  • technical reports and other articles issued by M‰lardalen University is free for personal use. For other use, the explicit consent of the authors is required
  • in other cases, please contact the copyright owner for detailed information

By accepting I agree to acknowledge and respect the rights of the copyright owner of the document I am about to access.

If you are in doubt, feel free to contact webmaster@ide.mdh.se

Bridging Function Block Diagrams and Verified Python Code: A Verification-Aware Approach for Programmable Logic Controllers

Fulltext:


Authors:

Mikael Ebrahimi Salari, Cristina Seceleanu, Eduard Paul Enoiu, Marco Eilers , Alessio Bucaioni, Wasif Afzal

Research group:

Industrial Software Engineering

Publication Type:

Conference/Workshop Paper

Abstract

Translating programmable logic controller (PLC) programs into analyzable artifacts can enable modern testing and verification techniques in industrial settings. PLC Function Block Diagram (FBD) programs differ from traditional software because they execute cyclically over physical inputs and outputs, combine signal flow with stateful and timed blocks, and depend on scan-cycle semantics, environment assumptions, and block-level abstractions. This paper presents a Python-based verification approach that combines PyLC+, a translation framework for IEC 61131-3 FBDs, with the Nagini verifier. PyLC+ extracts block networks from PLCopen XML and generates executable Python models that preserve the extracted topology, signal flow, and scan-cycle ordering, while making vendor-specific semantics explicit through reconstruction or abstraction. We apply the approach to 13 industrial program organization units (POUs), where 12 are verified against concrete or partially abstracted FBD-derived models, and one against an abstract requirements-level specification. The results provide evidence that automated extraction, manual semantic completion, and contract-based specification can support deductive verification of realistic POU-level models. The guarantees apply to the stated verification models, not to the full original PLC logic including all vendor-specific and timing semantics.We discuss the required abstractions, a Nagini issue exposed by one POU, and missing block semantics that currently limit further automation in PyLC+.

Bibtex

@inproceedings{Ebrahimi Salari7424,
author = {Mikael Ebrahimi Salari and Cristina Seceleanu and Eduard Paul Enoiu and Marco Eilers and Alessio Bucaioni and Wasif Afzal},
title = {Bridging Function Block Diagrams and Verified Python Code: A Verification-Aware Approach for Programmable Logic Controllers},
month = {October},
year = {2026},
url = {http://www.es.mdu.se/publications/7424-}
}