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

Direct link
Clocks, DBMs and States in Timed 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.
2002 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

Today, computers are used to control various technical systems in our society. In many cases, time plays a crucial role in the operation of computers embedded in such systems. This thesis is about techniques and tools for the analysis of timing behaviours of computer systems. Its main contributions are in the development and implementation of UPPAAL, a tool designed to automate the analysis process of systems modelled as timed automata.

As the first contribution, we present a software package for timing constraints represented as Difference Bound Matrices. We describe in details, all data-structures and operations for DBMs needed in state-space exploration of timed automata, as well as techniques for efficient implementation. In particular, we have developed two normalisation algorithms to guarantee termination of reachability analysis for timed automata containing constraints on clock differences, that transform DBMs according to not only maximal constants of clocks as in algorithms published in the literature, but also difference constraints appearing in the automata. The second contribution of this thesis is a collection of low level optimisations on the internal data-structures and algorithms of UPPAAL to minimise memory and time consumption. We present compression techniques to allow the state-space of a system to be efficiently stored and manipulated in main memory. We also study super-trace and hash-compaction methods for timed automata to deal with system-models for which the size of available memory is too small to store the explored state-space. Our experiments show that these techniques have greatly improved the performance of UPPAAL. The third contribution is in partial-order reduction techniques for timed-systems. A major problem in automatic verification is the large number of redundant states and transitions introduced by modelling concurrent events as interleaved transitions. We propose a notion of committed locations for timed automata. Committed locations are annotations that can be used for not only modelling of intermediate states within atomic transitions, but also guiding the model checker to ignore unnecessary interleavings in state-space exploration. The notion of committed locations has been generalised to give a local-time semantics for networks of timed automata, which allows for the application of existing partial order reduction techniques to timed systems.

Place, publisher, year, edition, pages
Uppsala: Acta Universitatis Upsaliensis , 2002. , 143 p.
Uppsala Dissertations from the Faculty of Science and Technology, ISSN 1104-2516 ; 39
National Category
Computer and Information Science
Research subject
Computer Science
URN: urn:nbn:se:uu:diva-2139ISBN: 91-554-5350-3OAI: oai:DiVA.org:uu-2139DiVA: diva2:161779
Public defence
2002-06-07, Polhemssalen, Ångströmlaboratoriet, Uppsala, 10:00
Available from: 2002-05-17 Created: 2002-05-17 Last updated: 2011-02-18Bibliographically approved

Open Access in DiVA

No full text
Buy this publication >>

By organisation
Division of Computer SystemsComputer Systems
Computer and Information 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: 575 hits
ReferencesLink to record
Permanent link

Direct link