• DocumentCode
    1491435
  • Title

    A protocol modeling and verification approach based on a specification language and Petri nets

  • Author

    Suzuki, Toshinori ; Shatz, Sol M. ; Murata, Tadao

  • Author_Institution
    Dept. of Electr. Eng. & Comput. Sci., Illinois Univ., Chicago, IL, USA
  • Volume
    16
  • Issue
    5
  • fYear
    1990
  • fDate
    5/1/1990 12:00:00 AM
  • Firstpage
    523
  • Lastpage
    536
  • Abstract
    An approach for automated modeling and verification of communication protocols is presented. A language that specifies the input/output behavior of protocol entities is introduced as the starting point of the approach, and verification of the linguistic specifications is discussed. Rules for conversion of the specifications into a Petri net model (based on a timed Petri net) are presented and illustrated by examples. This leads to a second level of verification on the net model. The approach is illustrated by its application to a part of the LAPD protocol
  • Keywords
    Petri nets; program verification; protocols; specification languages; LAPD protocol; Petri nets; automated modeling; communication protocols; conversion rules; input/output behavior; linguistic specifications; specification language; timed Petri net; verification; Automata; Computer science; Concurrent computing; Petri nets; Protocols; Software engineering; Specification languages; Time factors;
  • fLanguage
    English
  • Journal_Title
    Software Engineering, IEEE Transactions on
  • Publisher
    ieee
  • ISSN
    0098-5589
  • Type

    jour

  • DOI
    10.1109/32.52775
  • Filename
    52775