Marcel Christian Werner

• Programmable Logic Controllers (PLCs) are typically applied in industrial environments with real-time requirements. In many cases, PLC development is based on standards defined by the International Electrotechnical Commission (IEC), in particular IEC 61131-3. This standard describes various languages for developing Program Organization Units (POUs), including the textual language Structured Text (ST) and graphical Function Block Diagrams (FBDs), two languages that have become widely accepted and often used in real-world applications. POUs are typically used over a long period of time and extended incrementally. As a result, their structural complexity and the associated challenges such as maintainability and readability tend to increase. In addition, safety-critical applications require formal verification, which can be achieved by translating IEC 61131-3 POUs into formal models. This often results in domain-specific models for verification purposes only. Furthermore, the transition to other development approaches, such as model-based design or changes to hardware that is not IEC 61131-3 compliant, often requires that existing IEC 61131-3 POUs be partially or completely designed from scratch. In contrast, synchronous languages have proven to be efficient for the modeling and formal verification of reactive real-time systems in both research and industrial applications. Therefore, this thesis introduces several detailed transformations to translate existing ST- and FBD-based POUs into semantically equivalent synchronous models. These transformations allow POUs to be reused in a model-based design approach that supports formal verification. Furthermore, a formal methods-based optimization approach is introduced, which significantly reduces (on average) the structural complexity of real-world data-flow models such as FBDs. It is also shown how hierarchical statecharts can be derived from ST- and FBD-based models to provide an alternative graphical representation of the control flow. The correctness of these approaches is analyzed both theoretically, based on the syntax and formal semantics of the languages, and practically, based on appropriate IEC 61131-3 POUs, by integrating the transformation and optimization approaches into PLCreX, an application developed as part of this research.