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

M. Atif

    Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

    10 Citaten (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.
    Originele taal-2Engels
    TitelProceedings International Conference on Emerging Technologies (ICET 2009, Islamabad, Pakistan, October 19-20, 2009)
    UitgeverijInstitute of Electrical and Electronics Engineers
    ISBN van geprinte versie978-1-4244-5630-7
    StatusGepubliceerd - 2009


    Duik in de onderzoeksthema's van 'Analysis and verification of Two-Phase Commit & Three-Phase Commit Protocols'. Samen vormen ze een unieke vingerafdruk.

    Citeer dit