Diagnostic Model Checking for Real-Time Systems

Authors

  • Kim G. Larsen
  • Paul Pettersson
  • Wang Yi

DOI:

https://doi.org/10.7146/brics.v3i57.18682

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.

Downloads

Published

1996-06-27

How to Cite

Larsen, K. G., 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