Diagnostic Model-Checking for Real-Time Systems

) Kim G. Larsen y Paul Pettersson z Wang Yi z Uppsala University Uppaal 1 is a new tool suit for automatic verification of safety and bounded liveness properties of networks of timed automata [LPY95a, LPY95b]. 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 the graphical interface of Uppaal this diagnostic feature allows for a number of errors to be more easily detected and corrected. UPPAAL. Uppaal deals with the traditionally encountered state-explosion problem by combining on-the-fly verification with a new and coarser symbolic technique. The tool suit contains tools and features including: ffl a graphical interface (Autograph) allowing networks of timed automata to be defined by drawing, ffl an automatic compilation of the graphical definition into a textual format used by the model-checker, thus supporting the important princi..