Automated verification of an audio-control protocol using Uppaal

J. Bengtsson, A. Griffioen, K.J. Kristoffersen, K.G. Larsen, F. Larsson, P. Petterson, Wentao Yi

Research output: Contribution to journalArticleAcademicpeer-review

30 Citations (Scopus)
18 Downloads (Pure)

Abstract

In this paper we present a case-study in which the tool Uppaal is extended and applied to verify an audio-control protocol developed by Philips. The size of the protocol studied in this paper is significantly larger than case studies, including various abstract versions of the same protocol without bus-collision handling, reported previously in the community of real-time verification. We have checked that the protocol will function correctly if the timing error of its components is bound to ±5%, and incorrectly if the error is ±6%. In addition, using Uppaal’s ability of generating diagnostic traces, we have studied an erroneous version of the protocol actually implemented by Philips, and constructed a possible execution sequence explaining the error. During the case-study, Uppaal was extended with the notion of committed locations. It allows for accurate modelling of atomic behaviours, and more importantly, it is utilised to guide the state-space exploration of the model checker to avoid exploring unnecessary interleavings of independent transitions. Our experimental results demonstrate considerable time and space-savings of the modified model checking algorithm. In fact, due to the huge time and memory-requirement, it was impossible to check a simple reachability property of the protocol before the introduction of committed locations, and now it takes only seconds.
Original languageEnglish
Pages (from-to)163-181
JournalJournal of logic and algebraic programming
Volume52-53
DOIs
Publication statusPublished - 2002
Externally publishedYes

Fingerprint Dive into the research topics of 'Automated verification of an audio-control protocol using Uppaal'. Together they form a unique fingerprint.

Cite this