An Iterative Refinement Framework for Tighter Worst-Case Execution Time Calculation

This paper presents an iterative refinement framework for static WCET analysis based on implicit path enumeration technique (IPET). We check the feasibility of IPET solutions, convert infeasible solutions to path constraints to exclude them from the analysis, and recalculate estimates whenever new path constraints are added. This process is repeated until no more constraints are extracted or a predefined time limit is reached. Since infeasible path detection itself is an undecidable problem, we propose an approximate method that checks feasibility efficiently while preserving safeness of the results. Generated path constraints are free of disjunctions; thus, amenable to integer linear program (ILP) solvers, which are used in IPET. We demonstrated the effectiveness and efficiency by conducting an experiment, where a module of flight control software of a commercial satellite developed in Korea was used