Logotype Mälardalenn University

MRTC publications



Compositional and Symbolic Model-Checking of Real-Time Systems,

Full text:  
Authors: Kim Guldstrand Larsen (Aalborg University, Denmark), Paul Pettersson, Wang Yi (external)
Source: the 16th IEEE Real-Time Systems Symposium, p 76-87, Pisa, Italy
 

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. In this paper we attack these explosion problems by developing and combining {\sl compositional} and {\sl symbolic} model-checking techniques. The presented techniques provide the foundation for a new automatic verification tool UPPAAL. Experimental results indicate that UPPAAL performs time- and space-wise favorably compared with other real-time verification tools.
 

BibTeX entry

@inproceedings{Guldstrand_2863:1995,
   author = {Kim Guldstrand Larsen and Paul Pettersson and Wang Yi},
   title = { Compositional and Symbolic Model-Checking of Real-Time Systems, },
   booktitle = {the 16th IEEE Real-Time Systems Symposium},
   month = {December},
   year = {1995},
   pages = {76-87},
   url = {http://www.mrtc.mdh.se/index.php?choice=publications&id=2863},
}

  • Mälardalen University |
  • Box 883 |
  • 721 23 Västerås/Eskilstuna |
  • 021-101300, 016-153600 |
  • webmaster |
  • Latest update: 2012.08.24