Technical Report 2003-050

Hierarchical Modeling and Analysis of Timed Systems

Alexandre David

November 2003

Uppaal is a tool for model-checking real-time systems developed jointly by Uppsala University and Aalborg University. It has been applied successfully in case studies ranging from communication protocols to multimedia applications. The tool is designed to verify systems that can be modeled as networks of timed automata. But it lacks support for systems with hierarchical structures, which makes the construction of large models difficult. In this thesis we improve the efficiency of Uppaal with new data structures and extend its modeling language and its engine to support hierarchical constructs.

To investigate the limits of Uppaal, we model and analyze an industrial fieldbus communication protocol. To our knowledge, this case study is the largest application Uppaal has been confronted to and we managed to verify the models. However, the hierarchical structure of the protocol is encoded as a network of automata without hierarchy, which artificially complicates the model. It turns out that we need to improve performance and enrich the modeling language.

To attack the performance bottlenecks, we unify the two central structures of the Uppaal engine, the passed and waiting lists, and improve memory management to take advantage of data sharing between states. We present experimental results that demonstrate improvements by a factor 2 in time consumption and a factor 5 in memory consumption.

We enhance the modeling capabilities of Uppaal by extending its input language with hierarchical constructs to structure the models. We have developed a verification engine that supports modeling of hierarchical systems without penalty in performance. To further benefit from the structures of models, we present an approximation technique that utilizes hierarchy in verification.

Finally, we propose a new architecture to integrate the different verification techniques into a common framework. It is designed as a pipeline built with components that are changed to fit particular experimental configurations and to add new features. The new engine of Uppaal is based on this architecture. We believe that the architecture is applicable to other verification tools.

Note: PhD thesis

Available as compressed Postscript (652 kB, no cover), Postscript (2.87 MB, no cover), and PDF (1.67 MB, no cover)

Download BibTeX entry.