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

Uppsala University
Centrum voor Wiskunde en Informatica
Radboud University Nijmegen
Danish National Research Foundation

科研成果: 书/报告/会议事项章节 › 会议稿件 › 同行评审

66 引用（Scopus）

摘要

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.

源语言	英语
主期刊名	Computer Aided Verification - 8th International Conference, CAV 1996, Proceedings
编辑	Thomas A. Henzinger, Rajeev Alur
出版商	Springer Verlag
页	244-256
页数	13
ISBN（印刷版）	3540614745, 9783540614746
DOI	https://doi.org/10.1007/3-540-61474-5_73
出版状态	已出版 - 1996
已对外发布	是
活动	8th International Conference on Computer Aided Verification, CAV 1996 - New Brunswick, 美国期限: 31 7月 1996 → 3 8月 1996

出版系列

姓名	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
卷	1102
ISSN（印刷版）	0302-9743
ISSN（电子版）	1611-3349

会议

会议	8th International Conference on Computer Aided Verification, CAV 1996
国家/地区	美国
市	New Brunswick
时期	31/07/96 → 3/08/96

访问文件

10.1007/3-540-61474-5_73

其它文件与链接

链接到 Scopus 的出版物

引用此

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. 在 T. A. Henzinger, & R. Alur (编辑), Computer Aided Verification - 8th International Conference, CAV 1996, Proceedings (页码 244-256). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); 卷 1102). Springer Verlag. https://doi.org/10.1007/3-540-61474-5_73

Bengtsson, Johan ; Gritffioen, W. O.David ; Kristoffersen, Kåre J. 等. / Verification of an audio protocol with bus collision using UPPAAL. Computer Aided Verification - 8th International Conference, CAV 1996, Proceedings. 编辑 / Thomas A. Henzinger ; Rajeev Alur. Springer Verlag, 1996. 页码 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. 在 TA Henzinger & R Alur (编辑), 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), 卷 1102, Springer Verlag, 页码 244-256, 8th International Conference on Computer Aided Verification, CAV 1996, New Brunswick, 美国, 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. 等.
Computer Aided Verification - 8th International Conference, CAV 1996, Proceedings. 编辑 / Thomas A. Henzinger; Rajeev Alur. Springer Verlag, 1996. 页码 244-256 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); 卷 1102).

科研成果: 书/报告/会议事项章节 › 会议稿件 › 同行评审

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

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 等. Verification of an audio protocol with bus collision using UPPAAL. 在 Henzinger TA, Alur R, 编辑, Computer Aided Verification - 8th International Conference, CAV 1996, Proceedings. Springer Verlag. 1996. 页码 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

摘要

出版系列

会议

访问文件

其它文件与链接

指纹

引用此