Compositional and Symbolic Model-Checking of Real-Time Systems

Authors

  • Kim G. Larsen
  • Paul Pettersson
  • Wang Yi

DOI:

https://doi.org/10.7146/brics.v3i59.18770

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.

Downloads

Published

1996-06-29

How to Cite

Larsen, K. G., Pettersson, P., & Yi, W. (1996). Compositional and Symbolic Model-Checking of Real-Time Systems. BRICS Report Series, 3(59). https://doi.org/10.7146/brics.v3i59.18770