Diagnostic Model-Checking for Real-Time Systems

Uppaal is a new tool suit for automatic veri cation of networks of timed automata. In this paper we describe the diagnostic model-checking feature of Uppaal and illustrates its usefulness through the debugging of a version of the Philips Audio-Control Protocol. Together with a graphical interface of Uppaal this diagnostic feature allows for a number of errors to be more easily detected and corrected.

• Type: Conference
• Year: 1995
• Where: HYBRID
• Authors: Kim Guldstrand Larsen, Paul Pettersson, Wang Yi
• Keywords: Automatic Veri Cation, Control Systems, Diagnostic Model-checking Feature, HYBRID 1995, Philips Audio-Control Protocol