TY - GEN
T1 - Formal Verification of COCO Database Framework Using CSP
AU - Li, Peimu
AU - Yin, Jiaqi
AU - Zhu, Huibiao
N1 - Publisher Copyright:
© 2022 Knowledge Systems Institute Graduate School. All rights reserved.
PY - 2022
Y1 - 2022
N2 - Nowadays, many applications are built on distributed databases for scalability and high availability. Therefore, the architecture design of distributed databases needs to satisfy some functional properties to ensure that the database can perform transactions reliably and efficiently. COCO is a distributed OLTP database that supports epoch-based commit and replication and two variants of optimistic concurrency control which use physical time or logical time. In this paper, we first use process algebra CSP to model COCO's architecture. Then we use model checker PAT to verify seven properties, including deadlockfree, consistency, availability, partition tolerance (CAP), and basically availability, soft state, eventual consistency (BASE). The results show COCO's commit and replication protocol satisfy the CAP theorem, and two optimistic concurrency control variants satisfy the BASE theorem.
AB - Nowadays, many applications are built on distributed databases for scalability and high availability. Therefore, the architecture design of distributed databases needs to satisfy some functional properties to ensure that the database can perform transactions reliably and efficiently. COCO is a distributed OLTP database that supports epoch-based commit and replication and two variants of optimistic concurrency control which use physical time or logical time. In this paper, we first use process algebra CSP to model COCO's architecture. Then we use model checker PAT to verify seven properties, including deadlockfree, consistency, availability, partition tolerance (CAP), and basically availability, soft state, eventual consistency (BASE). The results show COCO's commit and replication protocol satisfy the CAP theorem, and two optimistic concurrency control variants satisfy the BASE theorem.
KW - COCO
KW - Distributed OLTP Database
KW - Modeling
KW - Process Algebra
KW - Verification
UR - http://www.scopus.com/inward/record.url?scp=85137152448&partnerID=8YFLogxK
U2 - 10.18293/SEKE2022-072
DO - 10.18293/SEKE2022-072
M3 - 会议稿件
AN - SCOPUS:85137152448
T3 - Proceedings of the International Conference on Software Engineering and Knowledge Engineering, SEKE
SP - 363
EP - 368
BT - SEKE 2022 - Proceedings of the 34th International Conference on Software Engineering and Knowledge Engineering
PB - Knowledge Systems Institute Graduate School
T2 - 34th International Conference on Software Engineering and Knowledge Engineering, SEKE 2022
Y2 - 1 July 2022 through 10 July 2022
ER -