zbMATH — the first resource for mathematics

Automated verification of an audio-control protocol using UPPAAL. (English) Zbl 1008.68009
Summary: 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 \(\pm 5\%\), and incorrectly if the error is \(\pm 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.

68M12 Network protocols
68Q60 Specification and verification (program logics, model checking, etc.)
Coq; HyTech; Kronos; Uppaal
Full Text: DOI
[1] Amnell, T.; Behrmann, G.; Bengtsson, J.; D’Argenio, P.R.; David, A.; Fehnker, A.; Hune, T.; Jeannet, B.; Larsen, K.G.; Möller, M.O.; Pettersson, P.; Weise, C.; Yi, W., \scuppaal—now, next, and future, (), 100-125
[2] Alur, R.; Dill, D., Automata for modelling real-time systems, (), 322-335 · Zbl 0765.68150
[3] Alur, R.; Kurshan, R.P., Timing analysis in COSPAN, (), 220-231
[4] Bengtsson, J.; David Griffioen, W.O.; Kristoffersen, K.J.; Larsen, K.G.; Larsson, F.; Pettersson, P.; Yi, W., Verification of an audio protocol with bus collision using \scuppaal, (), 244-256
[5] J. Bengtsson, F. Larsson, \scUppaal a tool for automatic verification of real-time systems, Master’s thesis, Uppsala University, 1996. Available from
[6] Bengtsson, J.; Larsen, K.G.; Larsson, F.; Pettersson, P.; Yi, W., \scuppaal—a tool suite for automatic verification of real – time systems, (), 232-243
[7] J. Bengtsson, K.G. Larsen, F. Larsson, P. Pettersson, W. Yi, C. Weise, New Generation of \scUppaal, in: International Workshop on Software Tools for Technology Transfer, June 1998
[8] D. Bosscher, I. Polak, F. Vaandrager, Verification of an audio-control protocol, in: Proceedings of Formal Techniques in Real-Time and Fault-Tolerant Systems, Lecture Notes in Computer Science, vol. 863, 1994
[9] Clarke, E.M.; Wing, J.M., Formal methods: state of the art and future directions, ACM computing surveys, 28, 4, 626-643, (1996)
[10] Daws, C.; Yovine, S., Two examples of verification of multirate timed automata with \sckronos, (), 66-75
[11] W.O. David Griffioen. Analysis of an Audio Control Protocol with Bus Collision, Master’s thesis, University of Amsterdam, Programming Research Group, 1994
[12] Henzinger, T.A.; Ho, P.-H.; Wong-Toi, H., \schytech: the next generation, (), 56-65
[13] Henzinger, T.A.; Ho, P.-H.; Wong-Toi, H., \schytech: a model checker for hybrid systems, International journal on software tools for technology transfer, 1, 1-2, 134-152, (1997)
[14] Henzinger, T.A.; Nicollin, X.; Sifakis, J.; Yovine, S., Symbolic model checking for real-time systems, Information and computation, 111, 2, 193-244, (1994) · Zbl 0806.68080
[15] Holzmann, G., The design and validation of computer protocols, (1991), Prentice Hall Englewood Cliffs, NJ
[16] Ho, P.-H.; Wong-Toi, H., Automated analysis of an audio control protocol, ()
[17] Larsson, F.; Larsen, K.G.; Pettersson, P.; Yi, W., Efficient verification of real-time systems: compact data structures and state-space reduction, (), 14-24
[18] Larsen, K.G.; Pettersson, P.; Yi, W., \scuppaal in a nutshell, International journal on software tools for technology transfer, 1, 1-2, 134-152, (1997) · Zbl 1060.68577
[19] Larsen, K.G.; Pettersson, P.; Yi, W., \scuppaal: status and developments, (), 456-459
[20] Larsen, K.G.; Steffen, B.; Weise, C., Continuous modeling of real-time and hybrid systems: from concepts to tools, International journal on software tools for technology transfer, 1, 1-2, 64-85, (1997) · Zbl 1060.68604
[21] Milner, R., Communication and concurrency, (1989), Prentice Hall Englewood Cliffs, NJ · Zbl 0683.68008
[22] LutjeSpelberg, R.F.; Toetenel, W.J., Parametric real-time model checking using splitting trees, Nordic journal, 8, 1, 88-120, (2001) · Zbl 0978.68098
[23] Yovine, S., A verification tool for real time systems, International journal on software tools for technology transfer, 1, 1-2, 134-152, (1997)
[24] Yi, W.; Pettersson, P.; Daniels, M., Automatic verification of real-time communicating systems by constraint-solving, (), 223-238
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.