Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Conference contribution/Paper › peer-review
Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Conference contribution/Paper › peer-review
}
TY - GEN
T1 - On simplifying modular specification and verification of distributed protocols
AU - Sinha, P.
AU - Suri, Neeraj
N1 - Cited By :8 Export Date: 7 October 2019
PY - 2001/10/22
Y1 - 2001/10/22
N2 - 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.
AB - 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.
KW - Chromium
KW - Protocols
KW - Systems engineering and theory
KW - Membership functions
KW - Network protocols
KW - Systems engineering
KW - Checkpointing protocol
KW - Design and analysis
KW - Distributed protocols
KW - Group membership protocols
KW - Inherent complexity
KW - Modular composition
KW - Modular specifications
KW - Systems engineering and theories
KW - Distributed computer systems
U2 - 10.1109/HASE.2001.966818
DO - 10.1109/HASE.2001.966818
M3 - Conference contribution/Paper
SN - 0769512755
SP - 173
EP - 181
BT - Proceedings Sixth IEEE International Symposium on High Assurance Systems Engineering
PB - IEEE
ER -