Diagnostic Model Checking for Real-Time Systems

  • Kim G. Larsen
  • Paul Pettersson
  • Wang Yi


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.
How to Cite
Larsen, K., Pettersson, P., & Yi, W. (1996). Diagnostic Model Checking for Real-Time Systems. BRICS Report Series, 3(57). https://doi.org/10.7146/brics.v3i57.18682