Counter Example Guided Abstraction Refinement for IEC 60848 GRAFCET

IEEE Industrial Electronics Society Annual On-Line Conference (ONCON), pp. 1–6

Abstract

This paper presents an application of counter example guided abstraction refinement to model checking of IEC 60848 GRAFCET for industrial control systems. We employ an abstraction technique tailored to GRAFCET in which transitions are replaced by abstract versions that disregard associated conditions and are fired non-deterministically. Furthermore, we abstract hierarchical elements, such as enclosures, by removing components of the GRAFCET specification. We present how counter examples can be used to refine the abstraction. While the computation of these counter examples can lead to an increase of verification time, evaluation shows that this technique can make model checking GRAFCET specifications more feasible.

Authors 7

1. Robin Mroß Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University,Embedded Software (Informatik 11),Aachen,Germany

2. Luca Söthe Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University,Embedded Software (Informatik 11),Aachen,Germany

3. Darko Divkovic

   Ruhr University Bochum

   Affiliation as printed

   Lehrstuhl für Automatisierungstechnik, Ruhr-Universität Bochum,Bochum,Germany

4. Aron Schnakenbeck

   Helmut Schmidt University

   Affiliation as printed

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

5. Marcus Völker Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University,Embedded Software (Informatik 11),Aachen,Germany

6. Alexander Fay

   Ruhr University Bochum

   Affiliation as printed

   Lehrstuhl für Automatisierungstechnik, Ruhr-Universität Bochum,Bochum,Germany

7. Stefan Kowalewski Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University,Embedded Software (Informatik 11),Aachen,Germany