Second International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS 2008) (VECoS)
Verification and Evaluation of Computer and Communication Systems
2 - 3 July 2008
We propose a novel formal method to compute an upper estimation of the WCET that contains the loss of precision and also can be easily parametrized by the hardware architecture. Assuming that there exists an executable timed model of the hardware, we first use symbolic execution  to precisely infer the execution time for a given instruction flow. We secondly identify execution states that can be merged with no loss of precision. Depending on the loss of precisionwe are ready to accept, we finally merge execution paths that have similar execution times.