Verifying the distributed real-time network protocol RTnet using Uppaal

F.T.Y. Hanssen; Angelika H. Mader; P.G. Jansen

doi:10.1109/MASCOTS.2006.52

Verifying the distributed real-time network protocol RTnet using Uppaal

F.T.Y. Hanssen, Angelika H. Mader, P.G. Jansen

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

264 Downloads (Pure)

Abstract

We present a formal analysis of RTnet using the model checker Uppaal. Besides normal protocol behaviour, the analysis focuses on the fault-handling properties of RTnet, in particular recovery after packet loss. Both qualitative and quantitative properties are presented, together with the verification results and conclusions about the robustness of RTnet.

Original language	Undefined
Title of host publication	Proceedings of the 14th IEEE/ACN International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems (MASCOTS)
Place of Publication	Los Alamitos
Publisher	IEEE
Pages	239-246
Number of pages	10
ISBN (Print)	0 7695 2573 3
DOIs	https://doi.org/10.1109/MASCOTS.2006.52
Publication status	Published - Jan 2006
Event	14th IEEE/ACN International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems, MASCOTS - Monterey, United States Duration: 11 Sept 2006 → 13 Sept 2006 Conference number: 14

Publication series

Name
Publisher	IEEE Computer Society

Conference

Conference	14th IEEE/ACN International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems, MASCOTS
Abbreviated title	MASCOTS
Country/Territory	United States
City	Monterey
Period	11/09/06 → 13/09/06

Keywords

IR-65608
EWI-2743
METIS-237431

Access to Document

10.1109/MASCOTS.2006.52

Cite this

@inproceedings{7e5548fbe9134dd988f66783e7b123ba,

title = "Verifying the distributed real-time network protocol RTnet using Uppaal",

abstract = "We present a formal analysis of RTnet using the model checker Uppaal. Besides normal protocol behaviour, the analysis focuses on the fault-handling properties of RTnet, in particular recovery after packet loss. Both qualitative and quantitative properties are presented, together with the verification results and conclusions about the robustness of RTnet.",

keywords = "IR-65608, EWI-2743, METIS-237431",

author = "F.T.Y. Hanssen and Mader, {Angelika H.} and P.G. Jansen",

note = "Imported from DIES; 14th IEEE/ACN International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems, MASCOTS ; Conference date: 11-09-2006 Through 13-09-2006",

year = "2006",

month = jan,

doi = "10.1109/MASCOTS.2006.52",

language = "Undefined",

isbn = "0 7695 2573 3",

publisher = "IEEE",

pages = "239--246",

booktitle = "Proceedings of the 14th IEEE/ACN International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems (MASCOTS)",

address = "United States",

}

Hanssen, FTY, Mader, AH & Jansen, PG 2006, Verifying the distributed real-time network protocol RTnet using Uppaal. in Proceedings of the 14th IEEE/ACN International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems (MASCOTS). IEEE, Los Alamitos, pp. 239-246, 14th IEEE/ACN International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems, MASCOTS, Monterey, Virginia, United States, 11/09/06. https://doi.org/10.1109/MASCOTS.2006.52

Verifying the distributed real-time network protocol RTnet using Uppaal. / Hanssen, F.T.Y.; Mader, Angelika H.; Jansen, P.G.
Proceedings of the 14th IEEE/ACN International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems (MASCOTS). Los Alamitos: IEEE, 2006. p. 239-246.

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

TY - GEN

T1 - Verifying the distributed real-time network protocol RTnet using Uppaal

AU - Hanssen, F.T.Y.

AU - Mader, Angelika H.

AU - Jansen, P.G.

N1 - Conference code: 14

PY - 2006/1

Y1 - 2006/1

N2 - We present a formal analysis of RTnet using the model checker Uppaal. Besides normal protocol behaviour, the analysis focuses on the fault-handling properties of RTnet, in particular recovery after packet loss. Both qualitative and quantitative properties are presented, together with the verification results and conclusions about the robustness of RTnet.

AB - We present a formal analysis of RTnet using the model checker Uppaal. Besides normal protocol behaviour, the analysis focuses on the fault-handling properties of RTnet, in particular recovery after packet loss. Both qualitative and quantitative properties are presented, together with the verification results and conclusions about the robustness of RTnet.

KW - IR-65608

KW - EWI-2743

KW - METIS-237431

U2 - 10.1109/MASCOTS.2006.52

DO - 10.1109/MASCOTS.2006.52

M3 - Conference contribution

SN - 0 7695 2573 3

SP - 239

EP - 246

BT - Proceedings of the 14th IEEE/ACN International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems (MASCOTS)

PB - IEEE

CY - Los Alamitos

T2 - 14th IEEE/ACN International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems, MASCOTS

Y2 - 11 September 2006 through 13 September 2006

ER -