Visualization and formalization of User Constraints for tight estimation of worst-case execution time

Automated static timing analysis methods provide a safe but usually overestimated worst-case execution time (WCET). Overestimation is mainly due to the existence of the execution paths that turn out to be infeasible or unrealistic when dynamic behavior of the program or environmental assumptions are fully considered. In this paper, we propose a new method and a visual language called User Constraint Language (UCL) to obtain a tight WCET estimation. In our method, both the program and flow information are represented by single formalism-finite automata. UCL provides intuitive visual notations with which users can easily specify various levels of flow information to characterize the execution paths of program. The user constraints specified in UCL are translated into finite automata. The combined automaton constructed by a cross-production of the automata for program and user constraints reflects the static structure and possible dynamic behavior of the program. It contains only the execution paths satisfying user constraints from which we can obtain a tight WCET using a path-based or Implicit Path Enumeration Technique (IPET)-based calculation method. A case study using part of a satellite flight software program demonstrates the effectiveness of UCL and our approach.