Home > Research > Publications & Outputs > On simplifying modular specification and verifi...


Text available via DOI:

View graph of relations

On simplifying modular specification and verification of distributed protocols

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSNConference contribution/Paperpeer-review

Publication date22/10/2001
Host publicationProceedings Sixth IEEE International Symposium on High Assurance Systems Engineering: Special Topic: Impact of Networking
Number of pages9
ISBN (Print)0769512755
<mark>Original language</mark>English


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. © 2001 IEEE.

Bibliographic note

Cited By :8 Export Date: 7 October 2019