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

Links

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

Published

Standard

On simplifying modular specification and verification of distributed protocols. / Sinha, P.; Suri, Neeraj.
Proceedings Sixth IEEE International Symposium on High Assurance Systems Engineering: Special Topic: Impact of Networking. IEEE, 2001. p. 173-181.

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

Harvard

Sinha, P & Suri, N 2001, On simplifying modular specification and verification of distributed protocols. in Proceedings Sixth IEEE International Symposium on High Assurance Systems Engineering: Special Topic: Impact of Networking. IEEE, pp. 173-181. https://doi.org/10.1109/HASE.2001.966818

APA

Sinha, P., & Suri, N. (2001). On simplifying modular specification and verification of distributed protocols. In Proceedings Sixth IEEE International Symposium on High Assurance Systems Engineering: Special Topic: Impact of Networking (pp. 173-181). IEEE. https://doi.org/10.1109/HASE.2001.966818

Vancouver

Sinha P, Suri N. On simplifying modular specification and verification of distributed protocols. In Proceedings Sixth IEEE International Symposium on High Assurance Systems Engineering: Special Topic: Impact of Networking. IEEE. 2001. p. 173-181 doi: 10.1109/HASE.2001.966818

Author

Sinha, P. ; Suri, Neeraj. / On simplifying modular specification and verification of distributed protocols. Proceedings Sixth IEEE International Symposium on High Assurance Systems Engineering: Special Topic: Impact of Networking. IEEE, 2001. pp. 173-181

Bibtex

@inproceedings{055cbda914864d92b5bc88c9c675409f,
title = "On simplifying modular specification and verification of distributed protocols",
abstract = "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. {\textcopyright} 2001 IEEE.",
keywords = "Chromium, Protocols, Systems engineering and theory, Membership functions, Network protocols, Systems engineering, Checkpointing protocol, Design and analysis, Distributed protocols, Group membership protocols, Inherent complexity, Modular composition, Modular specifications, Systems engineering and theories, Distributed computer systems",
author = "P. Sinha and Neeraj Suri",
note = "Cited By :8 Export Date: 7 October 2019",
year = "2001",
month = oct,
day = "22",
doi = "10.1109/HASE.2001.966818",
language = "English",
isbn = "0769512755",
pages = "173--181",
booktitle = "Proceedings Sixth IEEE International Symposium on High Assurance Systems Engineering",
publisher = "IEEE",

}

RIS

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 -