Open AccessDiagnostic Model Checking for Real-Time Systems
Author(s) -
Kim Guldstrand Larsen,
Paul Pettersson,
Yi Wang
Publication year - 1996
Publication title -
brics report series
Language(s) - English
Resource type - Journals
eISSN - 1601-5355
pISSN - 0909-0878
DOI - 10.7146/brics.v3i57.18682
Subject(s) - computer science , debugging , model checking , feature (linguistics) , automaton , protocol (science) , programming language , timed automaton , real time operating system , real time computing , embedded system , theoretical computer science , medicine , philosophy , linguistics , alternative medicine , pathology
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.