Model-Checking for Real-Time Systems

8 years 7 months ago
Model-Checking for Real-Time Systems
E cient 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 veri cation tool Uppaal . Experimental results show that Uppaal is not only substantially faster than other real-time veri cation tools but also able to handle much larger systems.
Rajeev Alur, Costas Courcoubetis, David L. Dill
Added 11 Aug 2010
Updated 11 Aug 2010
Type Conference
Year 1990
Where LICS
Authors Rajeev Alur, Costas Courcoubetis, David L. Dill
Comments (0)