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 {\em
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.