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 devoid of timing faults. The techniques to determine the tick length statically are classified as worst case reaction time (WCRT) analysis. 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 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 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. We then present an approach for static WCRT ana...

• Type: Conference
• Year: 2009
• Where: CASES
• Authors: Partha S. Roop, Sidharta Andalam, Reinhard von Hanxleden, Simon Yuan, Claus Traulsen
• Keywords: CASES 2009, Communications, Synchronous Programs, Tight Wcrt Value, WCRT Value