TY - CONF
T1 - Deriving a State Model of a Control Program by Symbolic Execution.
AU - Bohm, Thomas
AU - Pichler, Josef
AU - Prähofer, Herbert
N1 - Publisher Copyright:
© 2018 IEEE.
Copyright:
Copyright 2018 Elsevier B.V., All rights reserved.
PY - 2018/9/24
Y1 - 2018/9/24
N2 - This paper presents an approach for deriving a state transition model which represents the behavior of a control component using symbolic execution. Symbolic execution is a technique for executing a program using symbolic values for unknowns. It explores execution paths in a program and then uses a SAT/SMT solver to prove that paths are feasible. Further, the approach allows using constraints on the environment and simplifications with a widening operator similar to abstract interpretation.We present the formal foundation of the approach, depict the the tool implementation, present results from a preliminary evaluation, and discuss various application scenarios.
AB - This paper presents an approach for deriving a state transition model which represents the behavior of a control component using symbolic execution. Symbolic execution is a technique for executing a program using symbolic values for unknowns. It explores execution paths in a program and then uses a SAT/SMT solver to prove that paths are feasible. Further, the approach allows using constraints on the environment and simplifications with a widening operator similar to abstract interpretation.We present the formal foundation of the approach, depict the the tool implementation, present results from a preliminary evaluation, and discuss various application scenarios.
KW - Program comprehension
KW - Programmable logic controllers
KW - State transition model
KW - Symbolic execution
UR - http://www.scopus.com/inward/record.url?scp=85055591353&partnerID=8YFLogxK
U2 - 10.1109/INDIN.2018.8472013
DO - 10.1109/INDIN.2018.8472013
M3 - Paper
SP - 754
EP - 759
ER -