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.

• Type: Conference
• Year: 1990
• Where: LICS
• Authors: Rajeev Alur, Costas Courcoubetis, David L. Dill
• Keywords: Automated Reasoning, Automatic Veri Cation, LICS 1990, Model Checking, Veri Cation Tools