Modular composition and verification of transaction processing protocols

Establishing the correctness of reliable distributed protocols supporting critical applications necessitates modular/compositional approaches to tackle the inherent complexity of these protocols. Efforts involved in the specification and verification of these reliable distributed protocols can be considerably reduced if the protocol is composed utilizing smaller components (building-blocks) possessing individual functionalities that are integral parts of the overall protocol operation. In this paper we present the modular composition of a transaction processing protocol, namely the three-phase commit (3PC) protocol utilizing concepts of category theory. Specifically, we illustrate how the overall global properties of the protocol can be proved by utilizing constructs of local sub-properties of the inherent building blocks of the 3PC protocol.