Tight WCRT analysis of synchronous C programs

Accurate estimation of the tick length of a synchronous program is essential for efficient and predictable implementations that are de-void of timing faults. The techniques to determine the tick length statically are classified as worst case reaction time (WCRT) analy-sis. While a plethora of techniques exist for worst case execution time (WCET) analysis of procedural programs, there are only a handful of techniques for determining the WCRT value of synchronous programs. Most of these techniques produce overestimates and hence are unsuit-able for the design of systems that are predictable while being also efficient. In this paper, we present an approach for the accurate esti-mation of the exact WCRT value of a synchronous program, called its tight WCRT value, using model checking. For our input specifications we have selected a synchronous C based language called PRET-C that is designed for programming Precision Timed (PRET) architectures