Titelaufnahme

Titel
Symbolic methods for the timing analysis of programs / by Jakob Zwirchmayr
VerfasserZwirchmayr, Jakob
Begutachter / BegutachterinKovacs, Laura ; Knoop, Jens ; Rochange, Christine
Erschienen2013
UmfangVI, 105 S. : graph. Darst.
HochschulschriftWien, Techn. Univ., Diss., 2013
SpracheEnglisch
Bibl. ReferenzOeBB
DokumenttypDissertation
Schlagwörter (DE)wcet analyse / programmanalyse / zeitanalyse / schleifenschranken / praezise wcet schranken
Schlagwörter (EN)wcet analysis / program analysis / timing analysis / loop bounds / precise wcet bounds
Schlagwörter (GND)Programmanalyse / Worst-Case-Laufzeit / Schranke <Mathematik>
URNurn:nbn:at:at-ubtuw:1-62879 Persistent Identifier (URN)
Zugriffsbeschränkung
 Das Werk ist frei verfügbar
Dateien
Symbolic methods for the timing analysis of programs [1.21 mb]
Links
Nachweis
Klassifikation
Zusammenfassung (Deutsch)

In this thesis we present a method for proving WCET bounds precise. Our approach guarantees that the WCET bound is actually computed for a feasible trace in the system. Moreover, our method is able to improve the WCET analysis quality by reducing the required manual annotations and the imprecision of WCET estimates, automatically tightening the WCET bound until precise when necessary. For doing so, we apply and combine symbolic techniques from algorithmic combinatorics, computer algebra, automated theorem proving and for- mal methods. Such symbolic techniques usually yield good analysis information but are computationally expensive: symbolic execution, for example, requires path-wise execu- tion of the whole program. In order to overcome the computationally expensive costs of symbolic methods, our challenge is to identify and apply symbolic methods only on relevant program parts. This way, the precision of symbolic techniques is fully exploited while avoiding the computational costs of the underlying approaches.

Zusammenfassung (Englisch)

In this thesis we present a method for proving WCET bounds precise. Our approach guarantees that the WCET bound is actually computed for a feasible trace in the system. Moreover, our method is able to improve the WCET analysis quality by reducing the required manual annotations and the imprecision of WCET estimates, automatically tightening the WCET bound until precise when necessary. For doing so, we apply and combine symbolic techniques from algorithmic combinatorics, computer algebra, automated theorem proving and for- mal methods. Such symbolic techniques usually yield good analysis information but are computationally expensive: symbolic execution, for example, requires path-wise execu- tion of the whole program. In order to overcome the computationally expensive costs of symbolic methods, our challenge is to identify and apply symbolic methods only on relevant program parts. This way, the precision of symbolic techniques is fully exploited while avoiding the computational costs of the underlying approaches.