Exact High Level WCET Analysis of Synchronous Programs by Symbolic State Space Exploration
George Logothetis, Klaus Schneider · 2003
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.