Compositional and Symbolic Model-Checking of Real-Time Systems

Kim G. Larsen
Paul Pettersson
Wang Yi

December 1996


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 compositional and 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.

Available as PostScript, PDF.


Last modified: 2003-06-08 by webmaster.