Deadlock in Packet Switching Networks

Anna Stramaglia; Jeroen J.A. Keiren; Hans Zantema

doi:10.1007/978-3-030-89247-0_9

Deadlock in Packet Switching Networks

Anna Stramaglia (Corresponding author)
, Jeroen J.A. Keiren
, Hans Zantema

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

1 Citation (Scopus)

4 Downloads (Pure)

Abstract

A deadlock in a packet switching network is a state in which one or more messages have not yet reached their target, yet cannot progress any further. We formalize three different notions of deadlock in the context of packet switching networks, to which we refer as global, local and weak deadlock. We establish the precise relations between these notions, and prove they characterize different sets of deadlocks. Moreover, we implement checking of deadlock freedom of packet switching networks using the symbolic model checker nuXmv. We show experimentally that the implementation is effective at finding subtle deadlock situations in packet switching networks.

Original language	English
Title of host publication	Fundamentals of Software Engineering
Subtitle of host publication	9th International Conference, FSEN 2021, Virtual Event, May 19–21, 2021, Revised Selected Papers
Editors	Hossein Hojjat, Mieke Massink
Place of Publication	Cham
Publisher	Springer
Pages	127-141
Number of pages	15
ISBN (Electronic)	978-3-030-89247-0
ISBN (Print)	978-3-030-89246-3
DOIs	https://doi.org/10.1007/978-3-030-89247-0_9
Publication status	Published - 17 Oct 2021
Event	9th International Conference on Fundamentals of Software Engineering, FSEN 2021 - Virtual, Online Duration: 19 May 2021 → 21 May 2021

Publication series

Name	Lecture Notes in Computer Science (LNCS)
Volume	12818
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	9th International Conference on Fundamentals of Software Engineering, FSEN 2021
City	Virtual, Online
Period	19/05/21 → 21/05/21

Bibliographical note

Publisher Copyright:
© IFIP International Federation for Information Processing 2021

Keywords

Packet switching network
Deadlock
Model checking

Access to Document

10.1007/978-3-030-89247-0_9

pdfFinal published version, 416 KBLicence: TAVERNE

Cite this

Stramaglia, A., Keiren, J. J. A., & Zantema, H. (2021). Deadlock in Packet Switching Networks. In H. Hojjat, & M. Massink (Eds.), Fundamentals of Software Engineering: 9th International Conference, FSEN 2021, Virtual Event, May 19–21, 2021, Revised Selected Papers (pp. 127-141). (Lecture Notes in Computer Science (LNCS); Vol. 12818). Springer. https://doi.org/10.1007/978-3-030-89247-0_9

@inproceedings{dc9b08baac124efd976280d4004aa8cf,

title = "Deadlock in Packet Switching Networks",

abstract = "A deadlock in a packet switching network is a state in which one or more messages have not yet reached their target, yet cannot progress any further. We formalize three different notions of deadlock in the context of packet switching networks, to which we refer as global, local and weak deadlock. We establish the precise relations between these notions, and prove they characterize different sets of deadlocks. Moreover, we implement checking of deadlock freedom of packet switching networks using the symbolic model checker nuXmv. We show experimentally that the implementation is effective at finding subtle deadlock situations in packet switching networks.",

keywords = "Packet switching network, Deadlock, Model checking",

author = "Anna Stramaglia and Keiren, \{Jeroen J.A.\} and Hans Zantema",

note = "Publisher Copyright: {\textcopyright} IFIP International Federation for Information Processing 2021; 9th International Conference on Fundamentals of Software Engineering, FSEN 2021 ; Conference date: 19-05-2021 Through 21-05-2021",

year = "2021",

month = oct,

day = "17",

doi = "10.1007/978-3-030-89247-0\_9",

language = "English",

isbn = "978-3-030-89246-3",

series = "Lecture Notes in Computer Science (LNCS)",

publisher = "Springer",

pages = "127--141",

editor = "Hossein Hojjat and Mieke Massink",

booktitle = "Fundamentals of Software Engineering",

address = "Germany",

}

Stramaglia, A , Keiren, JJA & Zantema, H 2021, Deadlock in Packet Switching Networks. in H Hojjat & M Massink (eds), Fundamentals of Software Engineering: 9th International Conference, FSEN 2021, Virtual Event, May 19–21, 2021, Revised Selected Papers. Lecture Notes in Computer Science (LNCS), vol. 12818, Springer, Cham, pp. 127-141, 9th International Conference on Fundamentals of Software Engineering, FSEN 2021, Virtual, Online, 19/05/21. https://doi.org/10.1007/978-3-030-89247-0_9

Deadlock in Packet Switching Networks. / Stramaglia, Anna (Corresponding author); Keiren, Jeroen J.A.; Zantema, Hans.
Fundamentals of Software Engineering: 9th International Conference, FSEN 2021, Virtual Event, May 19–21, 2021, Revised Selected Papers. ed. / Hossein Hojjat; Mieke Massink. Cham: Springer, 2021. p. 127-141 (Lecture Notes in Computer Science (LNCS); Vol. 12818).

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

TY - GEN

T1 - Deadlock in Packet Switching Networks

AU - Stramaglia, Anna

AU - Keiren, Jeroen J.A.

AU - Zantema, Hans

PY - 2021/10/17

Y1 - 2021/10/17

N2 - A deadlock in a packet switching network is a state in which one or more messages have not yet reached their target, yet cannot progress any further. We formalize three different notions of deadlock in the context of packet switching networks, to which we refer as global, local and weak deadlock. We establish the precise relations between these notions, and prove they characterize different sets of deadlocks. Moreover, we implement checking of deadlock freedom of packet switching networks using the symbolic model checker nuXmv. We show experimentally that the implementation is effective at finding subtle deadlock situations in packet switching networks.

AB - A deadlock in a packet switching network is a state in which one or more messages have not yet reached their target, yet cannot progress any further. We formalize three different notions of deadlock in the context of packet switching networks, to which we refer as global, local and weak deadlock. We establish the precise relations between these notions, and prove they characterize different sets of deadlocks. Moreover, we implement checking of deadlock freedom of packet switching networks using the symbolic model checker nuXmv. We show experimentally that the implementation is effective at finding subtle deadlock situations in packet switching networks.

KW - Packet switching network

KW - Deadlock

KW - Model checking

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

U2 - 10.1007/978-3-030-89247-0_9

DO - 10.1007/978-3-030-89247-0_9

M3 - Conference contribution

SN - 978-3-030-89246-3

T3 - Lecture Notes in Computer Science (LNCS)

SP - 127

EP - 141

BT - Fundamentals of Software Engineering

A2 - Hojjat, Hossein

A2 - Massink, Mieke

PB - Springer

CY - Cham

T2 - 9th International Conference on Fundamentals of Software Engineering, FSEN 2021

Y2 - 19 May 2021 through 21 May 2021

ER -

Deadlock in Packet Switching Networks

Abstract

Publication series

Conference

Bibliographical note

Keywords

Access to Document

Other files and links

Fingerprint

Deadlock in packet switching networks

Cite this