Deriving a state model of a control program by symbolic execution
| H. Prähofer, T. Böhm, J. Pichler. Deriving a state model of a control program by symbolic execution. pages 754-759, DOI 10.1109/INDIN.2018.8472013, 9, 2018. | |
| Autoren | |
| Buch | Proceedings of the IEEE 16th International Conference on Industrial Informatics (INDIN 2018) |
| Typ | In Konferenzband |
| Verlag | IEEE |
| DOI | 10.1109/INDIN.2018.8472013 |
| ISBN | 978-1-5386-4829-2 |
| Monat | 9 |
| Jahr | 2018 |
| Seiten | 754-759 |
| Abstract | 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. |