Model Checking Generated Control Code for Consistency with its Specification in IEC 60848 GRAFCET

IFAC-PapersOnLine, vol. 58, pp. 264–269

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.

Authors 5

1. Robin Mroß corresponding Aachen Lehrstuhl Informatik 11

   RWTH Aachen University

   Affiliation as printed

   Lehrstuhl Informatik 11, RWTH Aachen University, 52074 Aachen, Germany

2. Aron Schnakenbeck corresponding

   Helmut Schmidt University

   Affiliation as printed

   Institut für Automatisierungstechnik, Helmut-Schmidt-Universität, 22043 Hamburg, Germany

3. Marcus Völker corresponding Aachen Lehrstuhl Informatik 11

   RWTH Aachen University

   Affiliation as printed

   Lehrstuhl Informatik 11, RWTH Aachen University, 52074 Aachen, Germany

4. Alexander Fay corresponding

   Helmut Schmidt University

   Affiliation as printed

   Institut für Automatisierungstechnik, Helmut-Schmidt-Universität, 22043 Hamburg, Germany

5. Stefan Kowalewski corresponding Aachen Lehrstuhl Informatik 11

   RWTH Aachen University

   Affiliation as printed

   Lehrstuhl Informatik 11, RWTH Aachen University, 52074 Aachen, Germany