Tight WCRT analysis of synchronous C programs

Accurate estimation of the tick length of a synchronous pro-gram is essential for efficient and predictable implementa-tions that are devoid of timing faults. The techniques to de-termine the tick length statically are classified as worst case reaction time (WCRT) analysis. While a plethora of tech-niques exist for worst case execution time (WCET) anal-ysis 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 unsuitable for the design of systems that are predictable while being also efficient. In this paper, we present an approach for the accurate estimation of the ex-act WCRT value of a synchronous program, called its tight WCRT value, using model checking. For our input speci