Verification of an audio protocol with bus collision using UPPAAL

Johan Bengtsson; W. O.David Gritffioen; Kåre J. Kristoffersen; Kim G. Larsen; Fredrik Larsson; Paul Pettersson; Wang Yi

doi:10.1007/3-540-61474-5_73

Verification of an audio protocol with bus collision using UPPAAL

Johan Bengtsson, W. O.David Gritffioen, Kåre J. Kristoffersen, Kim G. Larsen, Fredrik Larsson, Paul Pettersson, Wang Yi

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

66 Scopus citations

Abstract

In this paper we apply the tool UPPAAL 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.

Original language	English
Title of host publication	Computer Aided Verification - 8th International Conference, CAV 1996, Proceedings
Editors	Thomas A. Henzinger, Rajeev Alur
Publisher	Springer Verlag
Pages	244-256
Number of pages	13
ISBN (Print)	3540614745, 9783540614746
DOIs	https://doi.org/10.1007/3-540-61474-5_73
State	Published - 1996
Externally published	Yes
Event	8th International Conference on Computer Aided Verification, CAV 1996 - New Brunswick, United States Duration: 31 Jul 1996 → 3 Aug 1996

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	1102
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	8th International Conference on Computer Aided Verification, CAV 1996
Country/Territory	United States
City	New Brunswick
Period	31/07/96 → 3/08/96

Access to Document

10.1007/3-540-61474-5_73

Cite this

Bengtsson, J., Gritffioen, W. O. D., Kristoffersen, K. J., Larsen, K. G., Larsson, F., Pettersson, P., & Yi, W. (1996). Verification of an audio protocol with bus collision using UPPAAL. In T. A. Henzinger, & R. Alur (Eds.), Computer Aided Verification - 8th International Conference, CAV 1996, Proceedings (pp. 244-256). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1102). Springer Verlag. https://doi.org/10.1007/3-540-61474-5_73

Bengtsson, Johan ; Gritffioen, W. O.David ; Kristoffersen, Kåre J. et al. / Verification of an audio protocol with bus collision using UPPAAL. Computer Aided Verification - 8th International Conference, CAV 1996, Proceedings. editor / Thomas A. Henzinger ; Rajeev Alur. Springer Verlag, 1996. pp. 244-256 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{1bc08a113b18470dae02ab6e553e9181,

title = "Verification of an audio protocol with bus collision using UPPAAL",

abstract = "In this paper we apply the tool UPPAAL 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.",

author = "Johan Bengtsson and Gritffioen, \{W. O.David\} and Kristoffersen, \{K{\aa}re J.\} and Larsen, \{Kim G.\} and Fredrik Larsson and Paul Pettersson and Wang Yi",

note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 1996.; 8th International Conference on Computer Aided Verification, CAV 1996 ; Conference date: 31-07-1996 Through 03-08-1996",

year = "1996",

doi = "10.1007/3-540-61474-5\_73",

language = "英语",

isbn = "3540614745",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "244--256",

editor = "Henzinger, \{Thomas A.\} and Rajeev Alur",

booktitle = "Computer Aided Verification - 8th International Conference, CAV 1996, Proceedings",

address = "德国",

}

Bengtsson, J, Gritffioen, WOD, Kristoffersen, KJ, Larsen, KG, Larsson, F, Pettersson, P & Yi, W 1996, Verification of an audio protocol with bus collision using UPPAAL. in TA Henzinger & R Alur (eds), Computer Aided Verification - 8th International Conference, CAV 1996, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 1102, Springer Verlag, pp. 244-256, 8th International Conference on Computer Aided Verification, CAV 1996, New Brunswick, United States, 31/07/96. https://doi.org/10.1007/3-540-61474-5_73

Verification of an audio protocol with bus collision using UPPAAL. / Bengtsson, Johan; Gritffioen, W. O.David; Kristoffersen, Kåre J. et al.
Computer Aided Verification - 8th International Conference, CAV 1996, Proceedings. ed. / Thomas A. Henzinger; Rajeev Alur. Springer Verlag, 1996. p. 244-256 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1102).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Verification of an audio protocol with bus collision using UPPAAL

AU - Bengtsson, Johan

AU - Gritffioen, W. O.David

AU - Kristoffersen, Kåre J.

AU - Larsen, Kim G.

AU - Larsson, Fredrik

AU - Pettersson, Paul

AU - Yi, Wang

N1 - Publisher Copyright: © Springer-Verlag Berlin Heidelberg 1996.

PY - 1996

Y1 - 1996

N2 - In this paper we apply the tool UPPAAL 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.

AB - In this paper we apply the tool UPPAAL 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.

UR - https://www.scopus.com/pages/publications/84957375295

U2 - 10.1007/3-540-61474-5_73

DO - 10.1007/3-540-61474-5_73

M3 - 会议稿件

AN - SCOPUS:84957375295

SN - 3540614745

SN - 9783540614746

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 244

EP - 256

BT - Computer Aided Verification - 8th International Conference, CAV 1996, Proceedings

A2 - Henzinger, Thomas A.

A2 - Alur, Rajeev

PB - Springer Verlag

T2 - 8th International Conference on Computer Aided Verification, CAV 1996

Y2 - 31 July 1996 through 3 August 1996

ER -

Bengtsson J, Gritffioen WOD, Kristoffersen KJ, Larsen KG, Larsson F, Pettersson P et al. Verification of an audio protocol with bus collision using UPPAAL. In Henzinger TA, Alur R, editors, Computer Aided Verification - 8th International Conference, CAV 1996, Proceedings. Springer Verlag. 1996. p. 244-256. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/3-540-61474-5_73

Verification of an audio protocol with bus collision using UPPAAL

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this