From Imperative Sequential Structured Text Models to Synchronous Quartz and Sequentially Constructive Models

Abstract:
In the field of Programmable Logic Controllers (PLCs), Structured Text (ST) is one of the languages described in IEC 61131 for implementing PLC applications organized into Program Organization Units (POUs). So far, research has focused on formal verification of existing POUs, and PLC vendors and engineering tools are increasingly supporting the integration of model-based design features for new projects. These needs are already being met by frameworks for developing reactive real-time systems using synchronous languages. However, existing methods for formalizing ST-based POUs using synchronous languages often change the structure of the original ST model. Therefore, this paper presents a straightforward formalization approach for existing ST-based POUs in order to reuse them in model-based design and formal verification. In particular, we investigate the translation of ST models into synchronous QUARTZ and sequential constructive models. In this context, we define a structural operational semantics to evaluate our transformations. Furthermore, we demonstrate the applicability of our transformations using simple POUs.