Model checking generated control code for consistency with its specification in IEC 60848 GRAFCET

Mroß, Robin; Schnakenbeck, Aron; Völker, Marcus; Fay, Alexander; Kowalewski, Stefan

doi:10.1016/j.ifacol.2024.07.045

Model checking generated control code for consistency with its specification in IEC 60848 GRAFCET

Publication date

2024-07-17

Document type

Konferenzbeitrag

Author

Mroß, Robin

Schnakenbeck, Aron

Völker, Marcus

Fay, Alexander

Kowalewski, Stefan

Organisational unit

Automatisierungstechnik

DOI

10.1016/j.ifacol.2024.07.045

URI

https://openhsu.ub.hsu-hh.de/handle/10.24405/22854

Conference

17th IFAC Workshop on discrete Event Systems (WODES 2024) ; Rio de Janeiro, Brazil ; April 29 – May 1, 2024

Publisher

Elsevier

Series or journal

IFAC-PapersOnLine

ISSN

2405-8963

Periodical volume

58

Periodical issue

1

First page

264

Last page

269

Part of the university bibliography

✅

Language

English

Abstract

Formalisms such as IEC 60848 GRAFCET can be used for the specification of system behavior, as a basis for verification, and for automated code generation, e.g. to Structured Text (ST) according to IEC 61131-3. A possible procedure comprises the specification of the system, the verification of that model followed by automated code generation. However, the verification results can be rendered useless if the automated code generator introduces unintended, possibly faulty behavior. This paper discusses an approach of verifying the generated code in ST against its original specification in GRAFCET using model checking, using an existing code generator.

Version

Published version

Access right on openHSU

Metadata only access