Formal models of communication services: a case study
- 1 August 1993
- journal article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in Computer
- Vol. 26 (8) , 37-47
- https://doi.org/10.1109/2.223535
Abstract
Formal methods can play an important role in exploring new communication systems services. The telecommunications and data communications communities have long accepted the need for formally describing protocols, but only recently have they considered formally describing a service by abstracting specifications from a particular protocol that provides that service. Specifying a service at an abstract level meets two important needs: standardization and customization. The author presents a simplified atomic multicast as an example service and input/output automata for the formal model. He shows how to represent the service specification, a protocol, and implementations of that protocol. He also sketches how to prove the correctness of the protocol and implementation, that is, how to show that the specified service is actually provided.Keywords
This publication has 12 references indexed in Scilit:
- Introduction to the ISO specification language LOTOSPublished by Elsevier ,2003
- The impossibility of implementing reliable communication in the face of crashesJournal of the ACM, 1993
- Protocol verification made simple: a tutorialComputer Networks and ISDN Systems, 1993
- Lazy cachingACM Transactions on Programming Languages and Systems, 1993
- Using mappings to prove timing propertiesDistributed Computing, 1992
- A stepwise refinement heuristic for protocol constructionACM Transactions on Programming Languages and Systems, 1992
- Highly concurrent logically synchronous multicastDistributed Computing, 1991
- Lightweight causal and atomic group multicastACM Transactions on Computer Systems, 1991
- Process AlgebraPublished by Cambridge University Press (CUP) ,1990
- Hierarchical correctness proofs for distributed algorithmsPublished by Association for Computing Machinery (ACM) ,1987