Compositional and Symbolic Model-Checking of Real-Time Systems

Kim G. Larsen, Paul Pettersson, Wang Yi

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

Full Text:

PDF


DOI: http://dx.doi.org/10.7146/brics.v3i59.18770
This website uses cookies to allow us to see how the site is used. The cookies cannot identify you or any content at your own computer.
OK


ISSN: 0909-0878 

Hosted by the State and University Library and Aarhus University Library