Improving WCET Analysis Precision through Automata Product

Real-time scheduling of application requires sound estimation of the Worst-Case Execution Time (WCET) of each task. Part of the over-approximation introduced by the WCET analysis of a task comes from not taking into account the fact that the (implicit) worst-case execution path may be infeasible. This article does not address the question of finding infeasible paths but provides a new formalism of automata to describe sets of infeasible paths. This formalism combines the possibilities to express state-based path acceptance (like in regular automata), constraints on counters (in the Implicit Path Enumeration Technique fashion) and contexts of validity (like in State charts). We show the applicability of our proposal by performing infeasible paths aware WCET analyses within the OTAWA framework. We provide algorithms that transform the control flow graph and/or the constraints system supporting the WCET analysis in order to exclude the specified paths.