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

M. Atif

doi:10.1109/ICET.2009.5353152

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

M. Atif

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

10 Citations (Scopus)

Abstract

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 language	English
Title of host publication	Proceedings International Conference on Emerging Technologies (ICET 2009, Islamabad, Pakistan, October 19-20, 2009)
Publisher	Institute of Electrical and Electronics Engineers
Pages	326-331
ISBN (Print)	978-1-4244-5630-7
DOIs	https://doi.org/10.1109/ICET.2009.5353152
Publication status	Published - 2009

Access to Document

10.1109/ICET.2009.5353152

Cite this

@inproceedings{b7a1e614449a45f0be5ca898bfb824e2,

title = "Analysis and verification of Two-Phase Commit & Three-Phase Commit Protocols",

abstract = "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.",

author = "M. Atif",

year = "2009",

doi = "10.1109/ICET.2009.5353152",

language = "English",

isbn = "978-1-4244-5630-7",

pages = "326--331",

booktitle = "Proceedings International Conference on Emerging Technologies (ICET 2009, Islamabad, Pakistan, October 19-20, 2009)",

publisher = "Institute of Electrical and Electronics Engineers",

address = "United States",

}

Analysis and verification of Two-Phase Commit & Three-Phase Commit Protocols. / Atif, M.
Proceedings International Conference on Emerging Technologies (ICET 2009, Islamabad, Pakistan, October 19-20, 2009). Institute of Electrical and Electronics Engineers, 2009. p. 326-331.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

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

AU - Atif, M.

PY - 2009

Y1 - 2009

N2 - 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.

AB - 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.

U2 - 10.1109/ICET.2009.5353152

DO - 10.1109/ICET.2009.5353152

M3 - Conference contribution

SN - 978-1-4244-5630-7

SP - 326

EP - 331

BT - Proceedings International Conference on Emerging Technologies (ICET 2009, Islamabad, Pakistan, October 19-20, 2009)

PB - Institute of Electrical and Electronics Engineers

ER -

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

Abstract

Access to Document

Fingerprint

Cite this