Analysis and verification of Two-Phase Commit & Three-Phase Commit Protocols

M. Atif

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    10 Citations (Scopus)


    This paper introduces a formal model of the distributed commit protocols in the process algebra mCRL2 and also their general requirements in the modal µ-calculus. We show how to make straightforward models of protocols and by doing so, how it becomes easy to identify problems. We apply this to the well-known Two-Phase Commit Protocol (2PC) and prove it problematic for single site failure. We also apply our method to its "amended" variant, the Three-Phase Commit Protocol (3PC) and prove it to be erroneous for simultaneous site failures. We present 2PC and 3PC in different communication settings and verify them with respect to their requirements.
    Original languageEnglish
    Title of host publicationProceedings International Conference on Emerging Technologies (ICET 2009, Islamabad, Pakistan, October 19-20, 2009)
    PublisherInstitute of Electrical and Electronics Engineers
    ISBN (Print)978-1-4244-5630-7
    Publication statusPublished - 2009


    Dive into the research topics of 'Analysis and verification of Two-Phase Commit & Three-Phase Commit Protocols'. Together they form a unique fingerprint.

    Cite this