Titelaufnahme

Diese Arbeit beschreibt die Realisierung einer Werkzeugkette für die statische Analyse von Steuerungsprogrammen in der Programmiersprache C. Mit dieser Werkzeugkette wird das Ziel verfolgt, für C-Steuerungsprogramme Modellabstraktionen zu bilden und damit ein besseres Programmverständnis zu erreichen. Aufbauend auf bestehenden Analysemethoden und unter Einsatz des Analysewerkzeuges Frame-C werden unterschiedliche Modellrepräsentationen, wie ein Abstrakter Syntaxbaum, Wertmengen für Variabeln und Kontrollussgraphen, erstellt. Diese Modelle werden dann weiterverwendet, um eine symbolische Ausführung des Programmes durchzuführen, welche alle möglichen Pfade des Programms identiziert und deren Bedingun- gen bestimmt. Zum Bestimmen der Lösbarkeit von logischen Pfadbedingungen wird der The- orembeweiser Z3 verwendet. Durch mehrfaches symbolisches Ausführen des Programmes wird schließlich ein Zustandsdiagramm erstellt, welches das reaktive Verhalten des Steuerungspro- gramms darstellt. Die Analyseergebnisse können nun dazu verwendet werden, um das kom- plexe Verhalten von Steuerungsprogrammen entsprechend darzustellen und den Entwicklern eine bessere Übersicht und besseres Verständnis über das Verhalten des Programms zu vermit- teln.

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 dierent analysis methods, the tool chain allows analyzing program code and creating dierent abstract model representations, such as an abstract syntax tree, value sets and a control ow 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 identies 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 nally help developers in analyzing and understanding the behavior of complex control programs.