Diagnostic Model-Checking for Real-Time Systems

Kim G. Larsen
Paul Pettersson
Wang Yi

December 1996


UPPAAL is a new tool suit for automatic verification 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

Available as PostScript, PDF.


Last modified: 2003-06-08 by webmaster.