A dissertation in Computer Systems for the degree of Doctor of Philosophy. Publicly examined in room X, Uppsala University, 19 February 1999. Technical Report DoCS 99/101. ISSN 0283-0574.

ABSTRACT

During the last decade, model-checking techniques for the verification of timed systems have been developed based 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.

THESIS

The whole thesis can be obtained as a gzipped postscript file (.ps.gz) or as a pdf file (.pdf). Parts of the thesis can be obtained below:

• PART I: Introduction
  • Abstract, Table of Contents and Introduction (ps.gz, pdf),
• PART II: Algorithms and Data Structures
  • Paper A: Automatic Verification of Real-Time Communicating Systems by Constraint-Solving (ps.gz, pdf),
  • Paper B: Compositional and Symbolic Model-Checking of Real-Time Systems (ps.gz, pdf),
  • Paper C: Diagnostic Model-Checking for Real-Time Systems (ps.gz, pdf),
  • Paper D:, Efficient Verification of Real-Time Systems: Compact Data-Structures and State-Space Reduction (ps.gz, pdf),
• PART III: Case Studies
  • Paper E: Automated Analysis of an Audio-Control Protocol Using UPPAAL (ps.gz, pdf),
  • Paper F: Formal Verification of a TDMA Protocol Startup Mechanism (ps.gz, pdf),
  • Paper G: Formal Design and Analysis of a Gear Controller (ps.gz, pdf),

Please also download the errata which contains some minor corrections to the thesis (.ps.gz, .pdf).

Hardcopies of the thesis are available from Department of Computer Systems, Uppsala University, P.O. Box 325, SE-751 05 Uppsala, Sweden.