A tool chain for analysis and model abstraction of C control programs
|Title||A tool chain for analysis and model abstraction of C control programs|
|Institution||Master's Program Computer Science|
|School||Johannes Kepler University Linz|
This thesis describes the implementation of a tool chain which allows the analysis of C control programs for the purpose of program understanding and model abstraction. Relying in different analysis methods, the tool chain allows analyzing program code and creating different abstract model representations, such as an abstract syntax tree, value sets and a control flow graph. For acquiring those basic model representations, the Frama-C analysis framework has been used. Further, those models are then used to perform a symbolic execution of the program, which identifies all paths of the program and retrieves the conditions for each path. The theorem prover Z3 is used to determine the solvability of the paths. By performing the symbolic execution multiple times, a state model of the program can be created. The analysis results, in particular, the created model representations and the state model, can finally help developers in analyzing and understanding the behavior of complex control programs.