Transformation of GRAFCET Into GAL for Verification Purposes Based on a Detailed Meta-Model

The graphical modeling language GRAFCET is used as a formal specification language in industrial control design. To use these formal specifications for model-driven development of control code it is beneficial to ensure their syntactical and semantic correctness. Therefore in this paper, a detailed...

Full description

Bibliographic Details
Main Authors: Robin Mross, Aron Schnakenbeck, Marcus Volker, Alexander Fay, Stefan Kowalewski
Format: Article
Language:English
Published: IEEE 2022-01-01
Series:IEEE Access
Subjects:
Online Access:https://ieeexplore.ieee.org/document/9966565/
Description
Summary:The graphical modeling language GRAFCET is used as a formal specification language in industrial control design. To use these formal specifications for model-driven development of control code it is beneficial to ensure their syntactical and semantic correctness. Therefore in this paper, a detailed meta-model for GRAFCET is presented, which takes so-called terms into account, i.e. logical and arithmetic expressions in conditions and assignments. The meta-model and additionally proposed invariants allow the creation of syntactically correct GRAFCET instances. Based on this, a translation of GRAFCET to Guarded Action Language (GAL) is presented. The resulting transition system in GAL forms the basis for a semantic analysis of the GRAFCET instances by means of model checking in future research. Finally, the models are then employed for automatic code generation in Structured Text.
ISSN:2169-3536