On simplifying modular specification and verification of distributed protocols

Computer systems supporting high assurance and high consequences applications typically utilize dependable distributed protocols to manage system resources and to provide sustained delivery of services in the presence of failures. The inherent complexity entailed in the design and analysis of such protocols, is increasingly necessitating the use of formal techniques in establishing the correctness of the protocol level operations. Exploiting modular design aspects appearing in most dependable distributed protocols, we have introduced techniques utilizing concepts of category theory for constructing formal library routines of a set of constituent functional primitives, and their use in establishing the correctness of the protocol operation. In this paper, we develop on our proposed category-theory-based approach for modular composition through formulating (a) a group membership protocol which can also form the next hierarchical building blocks for other dependable protocol operations, and (b) a checkpointing protocol utilizing the group membership function as one of its building block. Subtleties in building-block interactions and their influence on the overall correctness of the composite protocols are also highlighted