Formal Description And Verification Of 2PCP Based On Asynchronous π-calculus

π-calculus, proposed by R. Milner and his fellows, is a name-passing calculus which is inherited from the development of CCS. It can naturally model concurrent systems which have dynamic communication structure, which is why it is called a calculus of mobile processes. The distinction ofπ-calculus comes from that it permits transmission of channel names between processes and can introduce and export local names. It is concise and has rich expression power,π-calculus has been used as an essential tool in studying concurrent communication systems. It is widely applied to formal description and verification of concurrent and distributed systems and communication protocols. The asynchronousπ-calculus is a variant of theπ-calculus where message emission is non-blocking.An atomic commitment protocol is an algorithm that ensures consistency. It is an algorithm for the coordinator and participants such that either, the coordinator and all participants commit the transaction, or they all abort it. The Two-Phase Commit Protocol is the simplest and most popular atomic commitment protocol. It guarantees the atomicity and durability in the commitment of distributed transactions. It permits any transaction manager to unilaterally decide to abort transactions which have not been committed.The purpose of this paper is to describe and verify the Two-Phase Commit Protocol based on asynchronousπ-calculus. In order to create more detailed, precise and integral work, we extend the asynchronousπ-calculus with1. site conception,2. the possibility of site failure and a persistence mechanism to deal with site failures,3. timer conception,4. the possibility of message loss and message duplication in inter-site communication.We discuss and analyze the Two-Phase Commit Protocol in several conditions (including, no any failure, site failure, message failure, etc.), and clearly and incrementally represent the two phase commit protocol in the asynchronousπ-calculus.The work of this paper indicates that the Two-Phase Commit Protocol can ensure the consistency in the distributed transaction processing. Blocking may occur only in a partial site failure or message failure, but the correctness is still assured.