• DocumentCode
    775739
  • Title

    On "A Simple Protocol Whose Proof Isńt": The State Machine Approach

  • Author

    Gouda, Mohamed G.

  • Author_Institution
    Univ. of Texas at Austin, Austin, TX
  • Volume
    33
  • Issue
    4
  • fYear
    1985
  • fDate
    4/1/1985 12:00:00 AM
  • Firstpage
    380
  • Lastpage
    382
  • 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
    Automata; Communications Society; Data structures; Logic; Protocols; Reactive power; Registers; Safety;
  • fLanguage
    English
  • Journal_Title
    Communications, IEEE Transactions on
  • Publisher
    ieee
  • ISSN
    0090-6778
  • Type

    jour

  • DOI
    10.1109/TCOM.1985.1096296
  • Filename
    1096296
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=775739