Practical Verification of Real-time Systems

Alexandre David, Uppsala University

Available as pdf or ps.gz file
or contact Alexandre at

Opponent: Parosh Abdulla
TIME: 10.15-12, Friday, Oct 12, 2001
PLACE: Room 2347, Information Technology, DoCS, Uppsala University

Formal methods are becoming mature enough to be used on non trivial examples. They are particularly well fitted for real-time systems whose correctness is defined 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 verification 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 first 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.

ARTES project: Hierarchical Design and Analysis of Timed Systems

Reference: Alexandre David, Practical Verification of Real-time Systems. Licentiate Theses from the Department of Information Technology, 2001-13 October 2001. ISSN 1404-5117.

  Strategic Research