Issue No. 05 - May (1990 vol. 16)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/32.52775
<p>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.</p>
conversion rules; specification language; Petri nets; automated modeling; verification; communication protocols; input/output behavior; linguistic specifications; timed Petri net; LAPD protocol; Petri nets; program verification; protocols; specification languages.
T. Murata, T. Suzuki and S. Shatz, "A Protocol Modeling and Verification Approach Based on a Specification Language and Petri Nets," in IEEE Transactions on Software Engineering, vol. 16, no. , pp. 523-536, 1990.