TACO: A scalable framework for timing analysis and code optimization of synchronous programs

Static estimation of the Worst Case Reaction Time (WCRT) of synchronous programs is pivotal for designing hard-real time systems in these languages. The current approaches to WCRT estimation suffer from either large overestimation of the WCRT value or the state space explosion problem. In this paper, we present TACO: a framework that integrates model checking based WCRT estimation with code optimization techniques, which results in close to optimal WCRT estimates with orders of magnitude reduced worst case runtime complexity. Finally, the TACO framework also allows us to generate executables with a smaller overall memory footprint.