Treffer: Towards Source-Level Timing Analysis of Embedded Software Using Functional Verification Methods ; Quellcode-basierte Zeitanalyse eingebetteter Software mit Hilfe funktionaler Verifikationsmethoden

This thesis evaluates a source-level approach to estimating the worst-case execution time of software, leveraging recent tools from functional verification. Towards this, we automatically annotate the source code with processor timing models, and apply a combination of Abstract Interpretation and Model Checking to compute a precise estimate that is superior to existing approaches. We further introduce 'Timing Debugging', a novel process which enables the user to inspect the execution time in a debugger. ; Diese Arbeit evaluiert einen Quellcode-basierten Ansatz zur Schätzung der maximalen Ausführungszeit von Software, unter Ausnutzung neuester Methoden aus den Bereich der funktionalen Verifikation. Zu diesem Zweck erweitern wir den Quellcode mit Prozessormodellen und wenden eine Kombination von Abstrakter Interpretation und Model Checking an, um eine Ausführungszeit zu berechnen welche präziser als jene bestehender Lösungen ist. Weiterhin stellen wir "Timing Debugging" vor, ein neuartiges Verfahren welches es ermöglicht die Ausführungszeit in einem Debugger zu untersuchen.