摘要：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.
