Visualization and formalization of user constraints for a tight estimation of worst-case execution time

Abstract

Timing analysis is an essential process for development of real-time embedded system and knowledge about the worst-case execution time (WCET) is crucial to validation of temporal correctness of implemented system. Research on automated static timing analysis is actively in progress to complement limitation of traditional timing measurement method. Automated static timing analysis methods provide safe but usually overestimated worst-cast execution time (WCET). Overestimation is mainly due to the existence of execution paths which turn out to be infeasible or impractical if dynamic behaviors of a program or environmental assumptions are fully considered. Therefore, user annotation of additional flow information is required for static WCET analyzer to get a tighter WCET estimation. In this thesis, we propose a new method and a visual language, User Constraint Language (UCL), to facilitate the specification of user constraints. In our method, both 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 execution paths of program. User constraints specified in UCL formulas are converted into corresponding finite automata. They are combined with the automaton representing the control flow graph of a target program through cross production. The combined automaton reflects the static structure and possible dynamic behavior of the program, and does not contain infeasible or impractical execution paths that are the main cause of loose estimation of WCET. We describe the visual notation and textual formula of UCL with examples which illustrate their usage. Then we define the formal syntax and semantics of UCL and propose a translation scheme to convert UCL formulas into finite automata. We also present a method to check the consistency of user-provided UCL constraints. UCL can specify complex flow information to elimi...