|
Diagnostic Model-Checking for Real-Time Systems
Kim G. Larsen December 1996 |
Abstract: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. |