A Control Flow based Static Analysis of GRAFCET using Abstract Interpretation

RWTH Publications (RWTH Aachen)

Abstract

The graphical modeling language GRAFCET is used as a formal specification language in industrial control design. This paper proposes a static analysis approach based on the control flow of GRAFCET using abstract interpretation to allow verification on specification level. GRAFCET has different elements leading to concurrent behavior, which in general results in a large state space. To get precise results and reduce the state space, we propose an analysis suitable for GRAFCET instances without concurrent behavior. We point out how to check for the absence of concurrency and present a flow-sensitive analysis for these GRAFCET instances. The proposed approach is evaluated on an industrial-sized example.

Authors 5

1. Aron Schnakenbeck

   Universität Hamburg · Helmut Schmidt University

   Affiliation as printed

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

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

2. Robin Mroß Aachen Lehrstuhl Informatik 11

   RWTH Aachen University

   Affiliation as printed

   Lehrstuhl Informatik 11 RWTH Aachen University 52074 Aachen, Germany

3. Marcus Völker Aachen Lehrstuhl Informatik 11

   RWTH Aachen University

   Affiliation as printed

   Lehrstuhl Informatik 11 RWTH Aachen University 52074 Aachen, Germany

4. Stefan Kowalewski Aachen Lehrstuhl Informatik 11

   RWTH Aachen University

   Affiliation as printed

   Lehrstuhl Informatik

   Lehrstuhl Informatik 11 RWTH Aachen University 52074 Aachen, Germany

5. Alexander Fay

   Universität Hamburg · Helmut Schmidt University

   Affiliation as printed

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

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