On "A Simple Protocol Whose Proof Isńt": The State Machine Approach
- 1 April 1985
- journal article
- letter
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Communications
- Vol. 33 (4) , 380-382
- https://doi.org/10.1109/tcom.1985.1096296
Abstract
We discuss how to model a synchronous protocol (due to Aho, Ullman, and Yannakakis) using communicating finite state machines, and present a proof for its safety and liveness properties. Our proof is based on constructing a labeled finite reachability graph for the protocol. This reachability graph can be viewed as a sequential program whose safety and liveness properties can be stated and verified in a straightforward fashion.Keywords
This publication has 6 references indexed in Scilit:
- A Simple Protocol Whose Proof Isn'tIEEE Transactions on Communications, 1985
- A technique for proving liveness of communicating finite state machines with examplesPublished by Association for Computing Machinery (ACM) ,1984
- Modeling communications protocols by automataPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1979
- Formal Techniques for Protocol Specification and VerificationComputer, 1979
- An axiomatic basis for computer programmingCommunications of the ACM, 1969
- Assigning meanings to programsPublished by American Mathematical Society (AMS) ,1967