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

• 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.