uu.seUppsala University Publications
Change search
ReferencesLink to record
Permanent link

Direct link
Hierarchical Modeling and Analysis of Real Time Systems
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
2003 (English)Doctoral thesis, monograph (Other academic)
Abstract [en]

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.

Place, publisher, year, edition, pages
Uppsala: Institutionen för informationsteknologi , 2003. , 188 p.
Technical report / Department of Information Technology, Uppsala University, ISSN 1404-3203 ; 050
Keyword [en]
Computer Science with specialization in Real Time Systems
National Category
Computer Science
URN: urn:nbn:se:uu:diva-3780ISBN: 91-506-1722-2OAI: oai:DiVA.org:uu-3780DiVA: diva2:163675
Public defence
2003-11-26, Häggsalen, Ångström, Uppsala, 10:00
Available from: 2003-11-05 Created: 2003-11-05 Last updated: 2011-02-18Bibliographically approved

Open Access in DiVA

No full text

By organisation
Division of Computer SystemsComputer Systems
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Total: 771 hits
ReferencesLink to record
Permanent link

Direct link