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

Direct link
Modelling and Verification of Real-Time Systems Using Timed Automata: Theory and Practice
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Computer Systems.
1999 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

During the last decade, model-checking techniques for the verification of timed system have been developed baaed on the theory of timed automata. The practical limitation in applying these techniques to industrial-size systems is the huge amount of time and memory needed to explore and store the state-space of the system model.

In this thesis, we improve the current status of model-checking techniques for timed systems by developing symbolic, on-the-fly and compositional verification techniques for timed automata. A common characteristics of the model-checking techniques presented is that they use efficient constraint-solving techniques to symbolically represent and manipulate the state-space. To avoid construction of the full state-space of the system model two techniques are used: on-the-fly generation of the state-space and a compositional model-checking technique. The memory-usage is further reduced by developing a minimal and canonical data structure for the class of constraints used in the model-checking algorithm, which reduces the size of each individual state. Two other techniques to reduce the total number of states explored and stored during verification are also presented.

The developed techniques have been implemented in the verification tool UPPAAL. To demonstrate the potential applications of our model-checking techniques, we present three industrial-size case studies where the UPPAAL tool is applied.

Place, publisher, year, edition, pages
Department of Computer Systems, Uppsala University , 1999. , 30 p.
DoCS, ISSN 0283-0574 ; 101
National Category
Computer Engineering
Research subject
Computer Systems
URN: urn:nbn:se:uu:diva-1161ISBN: 99-2900552-8OAI: oai:DiVA.org:uu-1161DiVA: diva2:160712
Public defence
1999-02-19, Room X, Uppsala University, Uppsala, 10:00 (English)
Available from: 1999-01-29 Created: 1999-01-29 Last updated: 2015-01-30Bibliographically approved

Open Access in DiVA

No full text

Search in DiVA

By author/editor
Pettersson, Paul
By organisation
Department of Computer Systems
Computer Engineering

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: 521 hits
ReferencesLink to record
Permanent link

Direct link