The main goal of this project is the development of analysis and design techniques for assuring the robustness of timed systems. It is assumed that a timed system is de- signed within the framework of timed automata. When a timed automaton has been verified, the results of the verification should be insensitive to small imprecisions in e.g. clock speeds and system parameters. In such a case the system is said to be robust. Robustness is an important property as it is a prerequisite for being able to imple- ment a verified design in a reliable way. Apart from analysis techniques for checking the robustness of a system this project studies design techniques for solving identified problems with robustness. An analysis of the cyclic behaviour of timed automata will form the theoretical basis of these results, that will be extended to areas like priced timed automata, real-time testing and hybrid automata.

The final aim is to incorporate the results into a tool integrated with UPPAAL, a state-of-the-art model checking tool for timed automata.

This research takes inspiration from both formal methods and tools, and systems and control theory, which is reflected by the fact that this project is a joint collaboration between two groups in these respective areas.

Summary in Dutch