TY - GEN
T1 - Formal Modeling and Verification of AMQP Protocol Using Multiparty Session Types
AU - Liu, Huiying
AU - Zhu, Huibiao
AU - Chen, Sini
N1 - Publisher Copyright:
© 2025 Knowledge Systems Institute Graduate School. All rights reserved.
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 -