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...
| Main Authors: | , , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
IEEE
2022-01-01
|
| Series: | IEEE Access |
| Subjects: | |
| Online Access: | https://ieeexplore.ieee.org/document/9966565/ |
| _version_ | 1811311485306011648 |
|---|---|
| author | Robin Mross Aron Schnakenbeck Marcus Volker Alexander Fay Stefan Kowalewski |
| author_facet | Robin Mross Aron Schnakenbeck Marcus Volker Alexander Fay Stefan Kowalewski |
| author_sort | Robin Mross |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-13T10:18:34Z |
| format | Article |
| id | doaj.art-84b223b92dfb4fdf8378eed6da7bb924 |
| institution | Directory Open Access Journal |
| issn | 2169-3536 |
| language | English |
| last_indexed | 2024-04-13T10:18:34Z |
| publishDate | 2022-01-01 |
| publisher | IEEE |
| record_format | Article |
| series | IEEE Access |
| spelling | doaj.art-84b223b92dfb4fdf8378eed6da7bb9242022-12-22T02:50:34ZengIEEEIEEE Access2169-35362022-01-011012565212566510.1109/ACCESS.2022.32257369966565Transformation of GRAFCET Into GAL for Verification Purposes Based on a Detailed Meta-ModelRobin Mross0https://orcid.org/0000-0002-1007-5597Aron Schnakenbeck1https://orcid.org/0000-0002-3507-2851Marcus Volker2https://orcid.org/0000-0001-7348-0146Alexander Fay3https://orcid.org/0000-0002-1922-654XStefan Kowalewski4https://orcid.org/0000-0002-7184-4804Lehrstuhl Informatik 11, RWTH Aachen University, Aachen, GermanyInstitut für Automatisierungstechnik, Helmut-Schmidt-Universität, Hamburg, GermanyLehrstuhl Informatik 11, RWTH Aachen University, Aachen, GermanyInstitut für Automatisierungstechnik, Helmut-Schmidt-Universität, Hamburg, GermanyLehrstuhl Informatik 11, RWTH Aachen University, Aachen, GermanyThe 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.https://ieeexplore.ieee.org/document/9966565/Industry automationformal modelformal verificationmodel checkingmodel-driven engineeringGRAFCET |
| spellingShingle | Robin Mross Aron Schnakenbeck Marcus Volker Alexander Fay Stefan Kowalewski Transformation of GRAFCET Into GAL for Verification Purposes Based on a Detailed Meta-Model IEEE Access Industry automation formal model formal verification model checking model-driven engineering GRAFCET |
| title | Transformation of GRAFCET Into GAL for Verification Purposes Based on a Detailed Meta-Model |
| title_full | Transformation of GRAFCET Into GAL for Verification Purposes Based on a Detailed Meta-Model |
| title_fullStr | Transformation of GRAFCET Into GAL for Verification Purposes Based on a Detailed Meta-Model |
| title_full_unstemmed | Transformation of GRAFCET Into GAL for Verification Purposes Based on a Detailed Meta-Model |
| title_short | Transformation of GRAFCET Into GAL for Verification Purposes Based on a Detailed Meta-Model |
| title_sort | transformation of grafcet into gal for verification purposes based on a detailed meta model |
| topic | Industry automation formal model formal verification model checking model-driven engineering GRAFCET |
| url | https://ieeexplore.ieee.org/document/9966565/ |
| work_keys_str_mv | AT robinmross transformationofgrafcetintogalforverificationpurposesbasedonadetailedmetamodel AT aronschnakenbeck transformationofgrafcetintogalforverificationpurposesbasedonadetailedmetamodel AT marcusvolker transformationofgrafcetintogalforverificationpurposesbasedonadetailedmetamodel AT alexanderfay transformationofgrafcetintogalforverificationpurposesbasedonadetailedmetamodel AT stefankowalewski transformationofgrafcetintogalforverificationpurposesbasedonadetailedmetamodel |