Trace-Guided Synthesis of Reactive Behavior Models of Programmable Logic Controllers

Programmable Logic Controller (PLC) programs are programs that control physical devices by continuously reading sensor inputs and writing actuator outputs. A main challenge in designing and comprehending PLC programs is the emergent behavior which arises from the complex interaction between the dynamic behavior of the program and the physical device. In this paper we present an approach for building a formal model characterizing the reactive interaction behavior of a PLC program with the physical device it controls. Based on program recordings, first a model of the transition behavior of the program run is built. Then, using symbolic execution and a formal abstraction process, we generate a specification of the input/output behavior as a state model with transition labelings in terms of conditions on input values. We present the main ideas of the approach, a formal model for representing the reactive behavior, the abstraction process, and two application scenarios.