Formal Modeling and Verification of AMQP Protocol Using Multiparty Session Types

Huiying Liu; Huibiao Zhu; Sini Chen

doi:10.18293/SEKE2025-42

Formal Modeling and Verification of AMQP Protocol Using Multiparty Session Types

Huiying Liu
, Huibiao Zhu^*
, Sini Chen

^*Corresponding author for this work

East China Normal University

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

Abstract

The Advanced Message Queuing Protocol (AMQP), an application-layer protocol based on the publish/subscribe model, is widely used in the field of distributed communication. To verify the correctness of its messaging mechanism and crash-handling mechanism, this paper employs the Multiparty Session Types (MPST) theory and the mpstk toolkit to formally model and verify the AMQP protocol. This paper introduces crash scenarios into the AMQP protocol and verifies the safety, deadlock-freedom, and liveness of both the protocol’s messaging mechanism and crash-handling mechanism. The verification results demonstrate that the messaging mechanism and crash-handling mechanism of the AMQP protocol satisfy the aforementioned properties, proving its reliability.

Original language	English
Title of host publication	Proceedings - SEKE 2025
Subtitle of host publication	37th International Conference on Software Engineering and Knowledge Engineering
Publisher	Knowledge Systems Institute Graduate School
Pages	147-152
Number of pages	6
ISBN (Electronic)	1891706624
DOIs	https://doi.org/10.18293/SEKE2025-42
State	Published - 2025
Event	37th International Conference on Software Engineering and Knowledge Engineering, SEKE 2025 - Hybrid, Pompeii, Italy Duration: 29 Sep 2025 → 4 Oct 2025

Publication series

Name	Proceedings of the International Conference on Software Engineering and Knowledge Engineering, SEKE
ISSN (Print)	2325-9000
ISSN (Electronic)	2325-9086

Conference

Conference	37th International Conference on Software Engineering and Knowledge Engineering, SEKE 2025
Country/Territory	Italy
City	Hybrid, Pompeii
Period	29/09/25 → 4/10/25

Keywords

Advanced Message Queuing Protocol
Failure Handling
Model Checking
Multiparty Session Types
Process Calculi

Access to Document

10.18293/SEKE2025-42

Cite this

Liu, H., Zhu, H., & Chen, S. (2025). Formal Modeling and Verification of AMQP Protocol Using Multiparty Session Types. In Proceedings - SEKE 2025: 37th International Conference on Software Engineering and Knowledge Engineering (pp. 147-152). (Proceedings of the International Conference on Software Engineering and Knowledge Engineering, SEKE). Knowledge Systems Institute Graduate School. https://doi.org/10.18293/SEKE2025-42

Liu, Huiying ; Zhu, Huibiao ; Chen, Sini. / Formal Modeling and Verification of AMQP Protocol Using Multiparty Session Types. Proceedings - SEKE 2025: 37th International Conference on Software Engineering and Knowledge Engineering. Knowledge Systems Institute Graduate School, 2025. pp. 147-152 (Proceedings of the International Conference on Software Engineering and Knowledge Engineering, SEKE).

@inproceedings{6c40a30eeea24b67b887b28d68631c83,

title = "Formal Modeling and Verification of AMQP Protocol Using Multiparty Session Types",

abstract = "The Advanced Message Queuing Protocol (AMQP), an application-layer protocol based on the publish/subscribe model, is widely used in the field of distributed communication. To verify the correctness of its messaging mechanism and crash-handling mechanism, this paper employs the Multiparty Session Types (MPST) theory and the mpstk toolkit to formally model and verify the AMQP protocol. This paper introduces crash scenarios into the AMQP protocol and verifies the safety, deadlock-freedom, and liveness of both the protocol{\textquoteright}s messaging mechanism and crash-handling mechanism. The verification results demonstrate that the messaging mechanism and crash-handling mechanism of the AMQP protocol satisfy the aforementioned properties, proving its reliability.",

keywords = "Advanced Message Queuing Protocol, Failure Handling, Model Checking, Multiparty Session Types, Process Calculi",

author = "Huiying Liu and Huibiao Zhu and Sini Chen",

note = "Publisher Copyright: {\textcopyright} 2025 Knowledge Systems Institute Graduate School. All rights reserved.; 37th International Conference on Software Engineering and Knowledge Engineering, SEKE 2025 ; Conference date: 29-09-2025 Through 04-10-2025",

year = "2025",

doi = "10.18293/SEKE2025-42",

language = "英语",

series = "Proceedings of the International Conference on Software Engineering and Knowledge Engineering, SEKE",

publisher = "Knowledge Systems Institute Graduate School",

pages = "147--152",

booktitle = "Proceedings - SEKE 2025",

address = "美国",

}

Liu, H , Zhu, H & Chen, S 2025, Formal Modeling and Verification of AMQP Protocol Using Multiparty Session Types. in Proceedings - SEKE 2025: 37th International Conference on Software Engineering and Knowledge Engineering. Proceedings of the International Conference on Software Engineering and Knowledge Engineering, SEKE, Knowledge Systems Institute Graduate School, pp. 147-152, 37th International Conference on Software Engineering and Knowledge Engineering, SEKE 2025, Hybrid, Pompeii, Italy, 29/09/25. https://doi.org/10.18293/SEKE2025-42

Formal Modeling and Verification of AMQP Protocol Using Multiparty Session Types. / Liu, Huiying ; Zhu, Huibiao; Chen, Sini.
Proceedings - SEKE 2025: 37th International Conference on Software Engineering and Knowledge Engineering. Knowledge Systems Institute Graduate School, 2025. p. 147-152 (Proceedings of the International Conference on Software Engineering and Knowledge Engineering, SEKE).

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

TY - GEN

T1 - Formal Modeling and Verification of AMQP Protocol Using Multiparty Session Types

AU - Liu, Huiying

AU - Zhu, Huibiao

AU - Chen, Sini

PY - 2025

Y1 - 2025

N2 - The Advanced Message Queuing Protocol (AMQP), an application-layer protocol based on the publish/subscribe model, is widely used in the field of distributed communication. To verify the correctness of its messaging mechanism and crash-handling mechanism, this paper employs the Multiparty Session Types (MPST) theory and the mpstk toolkit to formally model and verify the AMQP protocol. This paper introduces crash scenarios into the AMQP protocol and verifies the safety, deadlock-freedom, and liveness of both the protocol’s messaging mechanism and crash-handling mechanism. The verification results demonstrate that the messaging mechanism and crash-handling mechanism of the AMQP protocol satisfy the aforementioned properties, proving its reliability.

AB - The Advanced Message Queuing Protocol (AMQP), an application-layer protocol based on the publish/subscribe model, is widely used in the field of distributed communication. To verify the correctness of its messaging mechanism and crash-handling mechanism, this paper employs the Multiparty Session Types (MPST) theory and the mpstk toolkit to formally model and verify the AMQP protocol. This paper introduces crash scenarios into the AMQP protocol and verifies the safety, deadlock-freedom, and liveness of both the protocol’s messaging mechanism and crash-handling mechanism. The verification results demonstrate that the messaging mechanism and crash-handling mechanism of the AMQP protocol satisfy the aforementioned properties, proving its reliability.

KW - Advanced Message Queuing Protocol

KW - Failure Handling

KW - Model Checking

KW - Multiparty Session Types

KW - Process Calculi

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

U2 - 10.18293/SEKE2025-42

DO - 10.18293/SEKE2025-42

M3 - 会议稿件

AN - SCOPUS:105018743400

T3 - Proceedings of the International Conference on Software Engineering and Knowledge Engineering, SEKE

SP - 147

EP - 152

BT - Proceedings - SEKE 2025

PB - Knowledge Systems Institute Graduate School

T2 - 37th International Conference on Software Engineering and Knowledge Engineering, SEKE 2025

Y2 - 29 September 2025 through 4 October 2025

ER -

Liu H , Zhu H, Chen S. Formal Modeling and Verification of AMQP Protocol Using Multiparty Session Types. In Proceedings - SEKE 2025: 37th International Conference on Software Engineering and Knowledge Engineering. Knowledge Systems Institute Graduate School. 2025. p. 147-152. (Proceedings of the International Conference on Software Engineering and Knowledge Engineering, SEKE). doi: 10.18293/SEKE2025-42

Formal Modeling and Verification of AMQP Protocol Using Multiparty Session Types

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this