Title: Symbolic methods for the timing analysis of programs
Language: English
Authors: Zwirchmayr, Jakob 
Qualification level: Doctoral
Advisor: Kovacs, Laura 
Assisting Advisor: Knoop, Jens 
Rochange, Christine 
Issue Date: 2013
Number of Pages: 105
Qualification level: Doctoral
Abstract: 
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.

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.
Keywords: wcet analyse; programmanalyse; zeitanalyse; schleifenschranken; praezise wcet schranken
wcet analysis; program analysis; timing analysis; loop bounds; precise wcet bounds
URI: http://media.obvsg.at/AC10775309-2001
Library ID: AC10775309
Organisation: E185 - Institut für Computersprachen 
Publication Type: Thesis
Hochschulschrift
Appears in Collections:Thesis

Files in this item:


Page view(s)

13
checked on Jul 17, 2021

Download(s)

12
checked on Jul 17, 2021

Google ScholarTM

Check


Items in reposiTUm are protected by copyright, with all rights reserved, unless otherwise indicated.