Assertional verification of a connection management protocol

András L. Oláh; Sonia M. Heemstra de Groot

doi:10.1007/978-0-387-34945-9_29

Assertional verification of a connection management protocol

András L. Oláh, Sonia M. Heemstra de Groot

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

4 Downloads (Pure)

Abstract

This paper deals with the verification of a connection management protocol which uses timestamps and network-wide synchronized clocks for the reliable opening and closing of connections. We prove the correctness of the protocol over an unreliable, bounded-delay network for the cases when (i) timestamps are unbounded; (ii) timestamps are from a finite modulo-N space. We determine the minimal safe value of N as a function of real-time parameters such as maximum packet lifetime, clock skew and maximum connection duration.

The protocol is modeled as a state-transition system and we argue about the properties of the system using an assertional technique based on temporal logic. Apart from handling safety and progress properties, this framework is also suitable to describe real-time aspects of the system.

Original language	English
Title of host publication	Formal Description Techniques VIII (FORTE '95)
Subtitle of host publication	Proceedings of the IFIP TC6 Eighth International Conference on Formal Description Techniques, Montreal, Canada, October 1995
Editors	Gregor von Bochmann, Rachida Dssouli, Omar Rafiq
Place of Publication	London
Publisher	Springer
Pages	401-416
ISBN (Electronic)	978-0-387-34945-9
ISBN (Print)	978-1-5041-2958-9
DOIs	https://doi.org/10.1007/978-0-387-34945-9_29
Publication status	Published - 12 Oct 1995
Event	IFIP TC6 8th International Conference on Formal Description Techniques, FORTE 1995 - Montreal, Canada Duration: 17 Oct 1995 → 20 Oct 1995 Conference number: 8

Publication series

Name	IFIP Advances in Information and Communication Technology
Publisher	Springer
ISSN (Print)	1868-4238
ISSN (Electronic)	1868-422X

Conference

Conference	IFIP TC6 8th International Conference on Formal Description Techniques, FORTE 1995
Abbreviated title	FORTE
Country	Canada
City	Montreal
Period	17/10/95 → 20/10/95

Keywords

Algebra
Communication
Information
Information processing
Telecommunications

Access to Document

10.1007/978-0-387-34945-9_29

Oldh1996assertionalFinal published version, 1.57 MB

Fingerprint Dive into the research topics of 'Assertional verification of a connection management protocol'. Together they form a unique fingerprint.

Cite this

Oláh, A. L., & Heemstra de Groot, S. M. (1995). Assertional verification of a connection management protocol. In G. von Bochmann, R. Dssouli, & O. Rafiq (Eds.), Formal Description Techniques VIII (FORTE '95): Proceedings of the IFIP TC6 Eighth International Conference on Formal Description Techniques, Montreal, Canada, October 1995 (pp. 401-416). (IFIP Advances in Information and Communication Technology). Springer. https://doi.org/10.1007/978-0-387-34945-9_29

Oláh, András L. ; Heemstra de Groot, Sonia M. / Assertional verification of a connection management protocol. Formal Description Techniques VIII (FORTE '95): Proceedings of the IFIP TC6 Eighth International Conference on Formal Description Techniques, Montreal, Canada, October 1995. editor / Gregor von Bochmann ; Rachida Dssouli ; Omar Rafiq. London : Springer, 1995. pp. 401-416 (IFIP Advances in Information and Communication Technology).

@inproceedings{8d87b37f213c4f1a8140211ccc5c05b9,

title = "Assertional verification of a connection management protocol",

abstract = "This paper deals with the verification of a connection management protocol which uses timestamps and network-wide synchronized clocks for the reliable opening and closing of connections. We prove the correctness of the protocol over an unreliable, bounded-delay network for the cases when (i) timestamps are unbounded; (ii) timestamps are from a finite modulo-N space. We determine the minimal safe value of N as a function of real-time parameters such as maximum packet lifetime, clock skew and maximum connection duration.The protocol is modeled as a state-transition system and we argue about the properties of the system using an assertional technique based on temporal logic. Apart from handling safety and progress properties, this framework is also suitable to describe real-time aspects of the system.",

keywords = "Algebra, Communication, Information, Information processing, Telecommunications",

author = "Ol{\'a}h, {Andr{\'a}s L.} and {Heemstra de Groot}, {Sonia M.}",

year = "1995",

month = oct,

day = "12",

doi = "10.1007/978-0-387-34945-9_29",

language = "English",

isbn = "978-1-5041-2958-9",

series = "IFIP Advances in Information and Communication Technology",

publisher = "Springer",

pages = "401--416",

editor = "{von Bochmann}, Gregor and Rachida Dssouli and Omar Rafiq",

booktitle = "Formal Description Techniques VIII (FORTE '95)",

note = "IFIP TC6 8th International Conference on Formal Description Techniques, FORTE 1995, FORTE ; Conference date: 17-10-1995 Through 20-10-1995",

}

Oláh, AL & Heemstra de Groot, SM 1995, Assertional verification of a connection management protocol. in G von Bochmann, R Dssouli & O Rafiq (eds), Formal Description Techniques VIII (FORTE '95): Proceedings of the IFIP TC6 Eighth International Conference on Formal Description Techniques, Montreal, Canada, October 1995. IFIP Advances in Information and Communication Technology, Springer, London, pp. 401-416, IFIP TC6 8th International Conference on Formal Description Techniques, FORTE 1995, Montreal, Canada, 17/10/95. https://doi.org/10.1007/978-0-387-34945-9_29

Assertional verification of a connection management protocol. / Oláh, András L.; Heemstra de Groot, Sonia M.

Formal Description Techniques VIII (FORTE '95): Proceedings of the IFIP TC6 Eighth International Conference on Formal Description Techniques, Montreal, Canada, October 1995. ed. / Gregor von Bochmann; Rachida Dssouli; Omar Rafiq. London : Springer, 1995. p. 401-416 (IFIP Advances in Information and Communication Technology).

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

TY - GEN

T1 - Assertional verification of a connection management protocol

AU - Oláh, András L.

AU - Heemstra de Groot, Sonia M.

N1 - Conference code: 8

PY - 1995/10/12

Y1 - 1995/10/12

N2 - This paper deals with the verification of a connection management protocol which uses timestamps and network-wide synchronized clocks for the reliable opening and closing of connections. We prove the correctness of the protocol over an unreliable, bounded-delay network for the cases when (i) timestamps are unbounded; (ii) timestamps are from a finite modulo-N space. We determine the minimal safe value of N as a function of real-time parameters such as maximum packet lifetime, clock skew and maximum connection duration.The protocol is modeled as a state-transition system and we argue about the properties of the system using an assertional technique based on temporal logic. Apart from handling safety and progress properties, this framework is also suitable to describe real-time aspects of the system.

AB - This paper deals with the verification of a connection management protocol which uses timestamps and network-wide synchronized clocks for the reliable opening and closing of connections. We prove the correctness of the protocol over an unreliable, bounded-delay network for the cases when (i) timestamps are unbounded; (ii) timestamps are from a finite modulo-N space. We determine the minimal safe value of N as a function of real-time parameters such as maximum packet lifetime, clock skew and maximum connection duration.The protocol is modeled as a state-transition system and we argue about the properties of the system using an assertional technique based on temporal logic. Apart from handling safety and progress properties, this framework is also suitable to describe real-time aspects of the system.

KW - Algebra

KW - Communication

KW - Information

KW - Information processing

KW - Telecommunications

U2 - 10.1007/978-0-387-34945-9_29

DO - 10.1007/978-0-387-34945-9_29

M3 - Conference contribution

SN - 978-1-5041-2958-9

T3 - IFIP Advances in Information and Communication Technology

SP - 401

EP - 416

BT - Formal Description Techniques VIII (FORTE '95)

A2 - von Bochmann, Gregor

A2 - Dssouli, Rachida

A2 - Rafiq, Omar

PB - Springer

CY - London

T2 - IFIP TC6 8th International Conference on Formal Description Techniques, FORTE 1995

Y2 - 17 October 1995 through 20 October 1995

ER -

Oláh AL, Heemstra de Groot SM. Assertional verification of a connection management protocol. In von Bochmann G, Dssouli R, Rafiq O, editors, Formal Description Techniques VIII (FORTE '95): Proceedings of the IFIP TC6 Eighth International Conference on Formal Description Techniques, Montreal, Canada, October 1995. London: Springer. 1995. p. 401-416. (IFIP Advances in Information and Communication Technology). https://doi.org/10.1007/978-0-387-34945-9_29