Automatic Error Cause Localization of Faulty PLC Programs

:When a model checker detects a violation of an all-quantified specification, it generates a counterexample trace that explains how to reach a violating state. In the context of PLCs, the counterexample contains the required stimuli for the program to cause erroneous behavior. Although these counterexamples are tremendously helpful to assess the violation, the actual cause of the erroneous behavior, i. e., the faulty line in the program, can be hidden anywhere in the counterexample trace. Finding the cause manually still takes great effort if the counterexample is long. In this paper, we present a technique to automatically find possible causes of such a violation of PLC programs running in cyclic scanning mode.