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.
|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|
|Publication status||Published - 2009|