Model-checking for real-time systems

  • Kim G. Larsen
  • , Paul Pettersson
  • , Wang Yi

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

152 Scopus citations

Abstract

Efficient automatic model-checking algorithms for real-time systems have been obtained in recent years based on the state-region graph technique of Alur, Courcoubetis and Dill. However, these algorithms are faced with two potential types of explosion arising from parallel composition: explosion in the space of control nodes, and explosion in the region space over clock-variables. This paper reports on work attacking these explosion problems by developing and combining compositional and symbolic model-checking techniques. The presented techniques provide the foundation for a new automatic verification tool UPPAAL. Experimental results show that UPPAAL is not only substantially faster than other real-time verification tools but also able to handle much larger systems.

Original languageEnglish
Title of host publicationFundamentals of Computation Theory - 10th International Conference, FCT 1995, Proceedings
EditorsHorst Reichel
PublisherSpringer Verlag
Pages62-88
Number of pages27
ISBN (Print)3540602496, 9783540602491
DOIs
StatePublished - 1995
Externally publishedYes
Event10th Conference on Fundamentals of Computation Theory, FCT 1995 - Dresden, Germany
Duration: 22 Aug 199525 Aug 1995

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume965
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference10th Conference on Fundamentals of Computation Theory, FCT 1995
Country/TerritoryGermany
CityDresden
Period22/08/9525/08/95

Fingerprint

Dive into the research topics of 'Model-checking for real-time systems'. Together they form a unique fingerprint.

Cite this