Deriving a State Model of a Control Program by Symbolic Execution
| Autor: | Josef Pichler, Herbert Prähofer, Thomas Bohm |
|---|---|
| Rok vydání: | 2018 |
| Předmět: |
Computer science
Programming language 020208 electrical & electronic engineering 020207 software engineering 02 engineering and technology Symbolic execution computer.software_genre Electronic mail Automaton Operator (computer programming) Unified Modeling Language Component (UML) Satisfiability modulo theories 0202 electrical engineering electronic engineering information engineering Computer Science::Programming Languages State (computer science) computer computer.programming_language |
| Zdroj: | INDIN |
| DOI: | 10.1109/indin.2018.8472013 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|