USING MODEL CHECKING TO DERIVE LOOP BOUNDS OF GENERAL LOOPS WITHIN ANSI-C APPLICATIONS FOR MEASUREMENT BASED WCET ANALYSIS 1

Knowing the boundaries of loops is an important prerequisite for both, static and dynamic Worst Case Execution Time (WCET) analysis. However, loop bound calculation is a complex task of its own, and often more effort than planned has to be put into it. This paper describes a simple and quick method for loop bound calculation using a model checker that cannot only find loop bounds for integer iterator variables but works with practically all kind of loops.