Loading
October 2001
Abstract: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.
Available as compressed Postscript (592 kB) and PDF (925 kB)
Download BibTeX entry.