Automatic Error Cause Localization of Faulty PLC Programs. Issue 7 (2015)

• Record Type: Journal Article
• Authors: Biallas, Sebastian; Friedrich, Nico; Simon, Hendrik; Kowalewski, Stefan
• Is Part Of: IFAC-PapersOnLine. Volume 48:Issue 7(2015)
• Page Start: 79
• Page End: 84
• Publication Date: 2015
• Subjects: Formal verification -- Programmable logic controllers -- Industry automation -- Software tools -- Software safety; Automatic control -- Periodicals; 629.805
• DOI: 10.1016/j.ifacol.2015.06.476
• Languages: English
• ISSNs: 2405-8963

Abstract

Abstract: 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.