Automatic Timing Model Generation by CFG Partitioning and Model Checking

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 run-time measurements. The measured times are used to calculate the WCET in a final computation step. As we operate on the 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.