Modeling And Verification Of Distributed Transactional System Based On CSP

Distributed transactional systems consist of distributed transactional memory and database systems.The former is designed to develop parallel programs and improve program execution efficiency,while the latter is designed to improve data storage efficiency and stability.DPSTM and COCO are two formalized systems in this field.DPSTM is a distributed Python software transactional memory that improves the efficiency of parallel programs developed using Python.COCO is a distributed OLTP database system designed for scalability and high availability to ensure reliable and efficient transaction processing.Formal modeling and verification of DPSTM and COCO are necessary due to the high system complexity,fault tolerance,and data consistency requirements of distributed transactional systems.Using formal methods can help developers and researchers discover potential issues in system design and implementation,improve system reliability and security,and provide an important guidance for distributed system design and implementation.The formal modeling and verification of DPSTM v2 architecture and COCO’s transaction commit protocols and optimistic concurrent control are conducted,and model checker PAT is used to verify properties such as deadlock freedom,ACID(Atomicity,Consistency,Isolation,Durability),sequential consistency,availability,read fault tolerance,and crash fault tolerance.The results show that DPSTM v2 and COCO distributed database system can operate distributed transactions efficiently and reliably.