Practical Verification of Real-Time Systems

Formal methods are becoming mature enough to be used on non trivial examples. They are par-ticularly well tted for real-time systems whose correctness is dened in terms of correct responses at correct times. Most common real-time systems are of reasonable size and can therefore be handled by an automatic verication tool such as Uppaal. Unfortunately the application of such techniques is not widely spread. This thesis presents advances in making formal techniques more accessable technology for system development and analysis. As the rst contribution, we report on an industrial case study to show that model checkers can be used for debugging and error localization. We shall present a number of abstraction techniques applied in the case study to avoid the state explosion problem. As the second contribution, we have developed a hierarchical extension of timed automata to enable more structured, compact, and more complex descriptions of systems by the users. Such a hierarchical representation is better suited for abstraction and expected to give better searching algorithms. Finally we present a hybrid animation system serving as a plug-in module for model-checkers to improve features for modelling and simulation