Abstract
In this paper we apply the tool Uppaal1 to an automatic analysis of a version of the Philips Audio Control Protocol with two senders and bus collision handling. This case study is significantly larger than the real-time/hybrid systems previously analysed by automatic tools. During the case study the tool Uppaal was extended with a new feature, committed locations, allowing efficient modelling of broadcast communication.
This work has been supported by the European Communities (under CONCUR2 and REACT), NUTEK (Swedish Board for Technical Development) TFR (Swedish Technical Research Council) and Netherlands Organization for Scientific Research (NWO) under contract SION 612-316-125.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
R. Alur and D. Dill. Automata for Modelling Real-Time Systems. In Proc. of ICALP'90, LNCS 443, 1990.
Johan Bengtsson and Fredrik Larsson. Uppaal a Tool for Automatic Verification of Real-time Systems, Master's thesis, Uppsala University, 1996.
Johan Bengtsson, Kim G. Larsen, Fredrik Larsson, Paul Pettersson, and Wang Yi. Uppaal — a Tool Suite for Automatic Verification of Real-Time Systems. In Proc. of the 4th DIMACS Workshop on Verification and Control of Hybrid Systems, 1995. To appear in LNCS, 1996.
D.J.B. Bosscher, I. Polak, and F.W. Vaandrager. Verification of an Audio-Control Protocol. In Proc. of FTRTFT'94, LNCS 863, pages 170–192, 1994.
C. Daws and S. Yovine. Two examples of verification of multirate timed automata with Kronos. In Proc. of the 16th IEEE Real-Time Systems Symposium, pages 66–75, December 1995.
W.O.D. Griffioen. Analysis of an Audio Control Protocol with Bus Collision. Master's thesis, University of Amsterdam, Programming Research Group, 1994.
Thomas A. Henzinger, Pei-Hsin Ho, and Howard Wong-Toi. HyTech: The Next Generation. In Proc. of the 16th IEEE Real-Time Systems Symposium, pages 56–65, December 1995.
N. Halbwachs, P. Raymond, and Y.-E. Proy. Verification of linear hybrid systems by means of convex approximations. In Static Analysis Symposium, LNCS 864, pages 223–237, 1994.
Pei-Hsin Ho and Howard Wong-Toi. Automated Analysis of an Audio Control Protocol. In Proc. of CAV'95, LNCS 939, 1995.
Kim G. Larsen, Paul Pettersson, and Wang Yi. Diagnostic Model-Checking for Real-Time Systems. In Proc. of the 4th DIMACS Workshop on Verification and Control of Hybrid Systems, 1995. To appear in LNCS, 1996.
Wang Yi, Paul Pettersson, and Mats Daniels. Automatic Verification of Real-Time Communicating Systems By Constraint-Solving. In Proc. of the 7th International Conference on Formal Description Techniques, 1994.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bengtsson, J. et al. (1996). Verification of an Audio Protocol with bus collision using Uppaal . In: Alur, R., Henzinger, T.A. (eds) Computer Aided Verification. CAV 1996. Lecture Notes in Computer Science, vol 1102. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61474-5_73
Download citation
DOI: https://doi.org/10.1007/3-540-61474-5_73
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61474-6
Online ISBN: 978-3-540-68599-9
eBook Packages: Springer Book Archive