Automatic timing model generation by CFG partitioning and model checking

In this paper we present a new measurement- based, worst-case execution time (WCET) analysis method. Exhaustive end-to-end measurements are computationally intractable in most cases. Therefore, we propose to measure execution times of subparts of the application. We use heuristic methods and model checking to generate test data, forcing the execution of selected paths to perform. runtime measurements. The measured times are used to calculate the WCET in a final computation step. As we operate on source code level our approach is platform independent except for the run time measurements performed on the target host. We show the feasibility of the required steps and explain our approach by means of a case study.