Abstract

Establishing the correctness of reliable distributed protocols supporting dependable 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 thesis, we introduce techniques utilizing the concepts of category theory for the modular composition of dependable distributed protocols. In particular, we show how by defining external interfaces of basic modules, and morphisms linking two different modules, a larger or more complex protocol can be formally composed and verified. To illustrate the effectiveness of the proposed methodology for compositional specification and verification, in this thesis, we present a modular composition and verification of a transaction processing protocol namely the non-blocking atomic three phase commit (3PC) protocol using category theoretic concepts. 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. A key benefit of this modular approach is that these identified building blocks would be helpful to system designers for their capability of specifying and facilitating rigorously tested and pretested formal theory modules of required system and component behavior; and also supporting system design decisions and modifications.