TY - GEN
T1 - Modeling and Analysis of RabbitMQ Using UPPAAL
AU - Li, Ran
AU - Yin, Jiaqi
AU - Zhu, Huibiao
N1 - Publisher Copyright:
© 2020 IEEE.
PY - 2020/12
Y1 - 2020/12
N2 - RabbitMQ is a very popular message middleware, which is an implementation of AMQP (Advanced Message Queuing Protocol) using the Erlang language. It supports concurrency and guarantees the sequential consistency of messages. Additionally, RabbitMQ provides the message acknowledgement mechanism to ensure that messages can be delivered reliably to the consumer from the broker. However, these crucial properties have not been verified with formal methods. In this paper, we model the architecture of RabbitMQ with timed automata. By utilizing the model checker UPPAAL, RabbitMQ is abstracted to five timed automata. Based on the formalized model, we verify whether RabbitMQ meets some essential properties, including Reachability of Data, Concurrency, Sequence Consistency and Message Acknowledgement. Consequently, it can be found that RabbitMQ can totally satisfy these properties according to the verification results via UPPAAL.
AB - RabbitMQ is a very popular message middleware, which is an implementation of AMQP (Advanced Message Queuing Protocol) using the Erlang language. It supports concurrency and guarantees the sequential consistency of messages. Additionally, RabbitMQ provides the message acknowledgement mechanism to ensure that messages can be delivered reliably to the consumer from the broker. However, these crucial properties have not been verified with formal methods. In this paper, we model the architecture of RabbitMQ with timed automata. By utilizing the model checker UPPAAL, RabbitMQ is abstracted to five timed automata. Based on the formalized model, we verify whether RabbitMQ meets some essential properties, including Reachability of Data, Concurrency, Sequence Consistency and Message Acknowledgement. Consequently, it can be found that RabbitMQ can totally satisfy these properties according to the verification results via UPPAAL.
KW - AMQP
KW - Modeling
KW - RabbitMQ
KW - UPPAAL
KW - Verification
UR - https://www.scopus.com/pages/publications/85101205281
U2 - 10.1109/TrustCom50675.2020.00024
DO - 10.1109/TrustCom50675.2020.00024
M3 - 会议稿件
AN - SCOPUS:85101205281
T3 - Proceedings - 2020 IEEE 19th International Conference on Trust, Security and Privacy in Computing and Communications, TrustCom 2020
SP - 79
EP - 86
BT - Proceedings - 2020 IEEE 19th International Conference on Trust, Security and Privacy in Computing and Communications, TrustCom 2020
A2 - Wang, Guojun
A2 - Ko, Ryan
A2 - Bhuiyan, Md Zakirul Alam
A2 - Pan, Yi
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 19th IEEE International Conference on Trust, Security and Privacy in Computing and Communications, TrustCom 2020
Y2 - 29 December 2020 through 1 January 2021
ER -