Title
Trace-Guided Synthesis of Reactive Behavior Models of Programmable Logic Controllers
Abstract
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.
Year
DOI
Venue
2013
10.1109/SEAA.2013.37
EUROMICRO-SEAA
Keywords
Field
DocType
dynamic behavior,reactive interaction behavior,reactive behavior,comprehending plc program,formal model,trace-guided synthesis,programmable logic controllers,reactive behavior models,transition behavior,physical device,plc program,output behavior,emergent behavior,sensor fusion,programmable controllers
Code coverage,Programming language,Abstraction,Computer science,Reverse engineering,Control engineering,Real-time computing,Sensor fusion,Software,Symbolic execution,Programmable logic controller,Program comprehension
Conference
Citations 
PageRank 
References 
1
0.41
11
Authors
2
Name
Order
Citations
PageRank
Roland Schatz1858.95
Herbert Prähofer218917.00