Comparison between static analysis and model checking in the design of automation systems

Control Engineering Practice, vol. 171, pp. 106813

Abstract

• Contribution to an IEC 60848 GRAFCET-based formal development process of control code. • Literature-based collection of properties relevant for verification. • Novel static analysis approach of GRAFCET using abstract interpretation. • Comparison of a model checking and a static analysis approach. Within the area of industrial control design, the standardized, graphical modeling language GRAFCET (IEC 60848) can be used not only for the specification of controllers, but also for model-driven development of control code. To this end, syntactical and semantic correctness of the model specified in GRAFCET is critical in order to obtain programs for PLCs that behave accordingly. To achieve this goal, this paper summarizes results of a research project investigating a tool chain for the formal verification of GRAFCET. This paper summarizes relevant properties to ensure correctness and two ways of inspecting the behavior of GRAFCET instances in order to check for these semantic properties are presented: one using static analysis techniques and one employing model checking, while discussing new details regarding static analysis techniques of concurrent elements in the models. By evaluating and comparing these two approaches, their respective strengths and weaknesses are assessed.

Authors 5

1. Aron Schnakenbeck corresponding

   Helmut Schmidt University

   Affiliation as printed

   Helmut-Schmidt-Universität/Universität der Bundeswehr Hamburg Institut für Automatisierungstechnik, Holstenhofweg 85, Hamburg, 22043, Germany

2. Robin Mroß Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University Lehrstuhl Informatik 11, Im Süsterfeld 9, Aachen, 52072, Germany

3. Marcus Völker Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University Lehrstuhl Informatik 11, Im Süsterfeld 9, Aachen, 52072, Germany

4. Stefan Kowalewski Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University Lehrstuhl Informatik 11, Im Süsterfeld 9, Aachen, 52072, Germany

5. Alexander Fay

   Ruhr University Bochum

   Affiliation as printed

   Ruhr-Universität Bochum Lehrstuhl Automatisierungstechnik, Universitätsstraße 150, Bochum, 44801, Germany