TY - GEN
T1 - Formalization and Verification of OpenStack Swift Using CSP
AU - Su, Ziqing
AU - Lin, Wei
AU - Zhu, Huibiao
N1 - Publisher Copyright:
© 2024 IEEE.
PY - 2024
Y1 - 2024
N2 - OpenStack Swift is an object storage system that is part of the open-source cloud platform OpenStack. It adopts a fully symmetric architecture design and is extensively employed in production environments to offer users highly available storage services. In this paper, we model OpenStack Swift's basic architecture, as well as its replication service using communication sequential processes (CSP). Additionally, we extend the audit service in Swift and provide a formal model of it. Various properties of our model are subsequently verified using the model checker PAT. The properties include Deadlock Freedom, Data Reachability, Consistency, Availability, Partition Tolerance (CAP), Basically Available, Soft State, Eventually Consistent (BASE), and Data Integrity. The verification results show that the design of OpenStack Swift satisfies both the CAP and the BASE theories and it achieves Data Integrity. In light of our results, it can be safely concluded that OpenStack Swift provides users with highly available and fault-tolerant services.
AB - OpenStack Swift is an object storage system that is part of the open-source cloud platform OpenStack. It adopts a fully symmetric architecture design and is extensively employed in production environments to offer users highly available storage services. In this paper, we model OpenStack Swift's basic architecture, as well as its replication service using communication sequential processes (CSP). Additionally, we extend the audit service in Swift and provide a formal model of it. Various properties of our model are subsequently verified using the model checker PAT. The properties include Deadlock Freedom, Data Reachability, Consistency, Availability, Partition Tolerance (CAP), Basically Available, Soft State, Eventually Consistent (BASE), and Data Integrity. The verification results show that the design of OpenStack Swift satisfies both the CAP and the BASE theories and it achieves Data Integrity. In light of our results, it can be safely concluded that OpenStack Swift provides users with highly available and fault-tolerant services.
KW - CSP
KW - Modeling
KW - OpenStack Swift
KW - Verification
UR - https://www.scopus.com/pages/publications/85204074661
U2 - 10.1109/COMPSAC61105.2024.00018
DO - 10.1109/COMPSAC61105.2024.00018
M3 - 会议稿件
AN - SCOPUS:85204074661
T3 - Proceedings - 2024 IEEE 48th Annual Computers, Software, and Applications Conference, COMPSAC 2024
SP - 51
EP - 60
BT - Proceedings - 2024 IEEE 48th Annual Computers, Software, and Applications Conference, COMPSAC 2024
A2 - Shahriar, Hossain
A2 - Ohsaki, Hiroyuki
A2 - Sharmin, Moushumi
A2 - Towey, Dave
A2 - Majumder, AKM Jahangir Alam
A2 - Hori, Yoshiaki
A2 - Yang, Ji-Jiang
A2 - Takemoto, Michiharu
A2 - Sakib, Nazmus
A2 - Banno, Ryohei
A2 - Ahamed, Sheikh Iqbal
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 48th IEEE Annual Computers, Software, and Applications Conference, COMPSAC 2024
Y2 - 2 July 2024 through 4 July 2024
ER -