Exact high level WCET analysis of synchronous programs by symbolic state space exploration

In this paper, a novel approach to high-level (i.e. architec-ture independent) worst case execution time (WCET) anal-ysis is presented that automatically computes exact bounds for all inputs. To this end, we make use of the distinc-tion between micro and macro steps as usually done by synchronous languages. As macro steps must not contain loops, a later low-level WCET analysis (architecture depen-dent) is simplified to a large extent. Checking exact execution times for all inputs is a com-plex task that can nevertheless be efficiently done when im-plicit state space representations are used. With our tools, it is not only possible to compute path information by explor-ing all computations, but also to verify given path informa-tion. 1