In: IEEE Transactions on Software Engineering, Vol. 16, No. 5, pages 523-536. May 1990.
Abstract: An approach for automated modeling and verification of communication protocols is presented. A language that specifies 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: communication protocol modelling (and) verification (based on a) specification language (and) net(s); timed net; LAPD protocol.