Algorithms and Tools for the Automatic Analysis of Embedded Systems.
Thomas A. Henzinger · 1997
Abstract : Over the past year, we developed and implemented new and improved formalisms and algorithms for the timing analysis and the analysis of environment interactions of embedded systems. Highlights include the first model-checking algorithm for timing constraints that is both on-the-fly and space-optimal; an extension of the formalism of timed and hybrid automata that enables modular design, specification, and analysis of embedded systems; an algorithm for the automatic synthesis of sampling controllers for continuous-time plants; and the automatic analysis of the steam-boiler benchmark case study with our model checker HyTech.