A Simple Protocol Whose Proof Isn't
- 1 April 1985
- journal article
- research article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Communications
- Vol. 33 (4) , 330-337
- https://doi.org/10.1109/tcom.1985.1096306
Abstract
Aho, Ullman, and Yannakakis have proposed a set of protocols that ensure reliable transmission of data across an error-prone channel. They have obtained lower bounds on the complexity required of the protocols to assure reliability for different classes of errors. They specify these protocols with finite-state machines. Although the protocol machines have only a small number of states, they are nontrivial to prove correct. In this paper we present proofs of one of these protocols using the finite-state-machine approach and the abstract-program approach. We also show that the abstract-program approach gives special insight into the operation of the protocol.Keywords
This publication has 28 references indexed in Scilit:
- On "A Simple Protocol Whose Proof Isńt": The State Machine ApproachIEEE Transactions on Communications, 1985
- Modular Verification of Computer Communication ProtocolsIEEE Transactions on Communications, 1983
- Specifying and Verifying Protocols Represented as Abstract ProgramsPublished by Springer Nature ,1982
- Verifying Concurrent Processes Using Temporal LogicPublished by Springer Nature ,1982
- "Sometime" is sometimes "not never"Published by Association for Computing Machinery (ACM) ,1980
- Formal Techniques for Protocol Specification and VerificationComputer, 1979
- Communicating sequential processesCommunications of the ACM, 1978
- A trivial algorithm whose analysis isn'tJournal of Computer and System Sciences, 1978
- Proving monitorsCommunications of the ACM, 1976
- An axiomatic basis for computer programmingCommunications of the ACM, 1969