Zwirchmayr, J. (2013). Symbolic methods for the timing analysis of programs [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2013.22070
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.<br />
de
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.<br />
