A protocol modeling and verification approach based on a specification language and Petri nets
T. Suzuki, Sol M. Shatz, Tadao Murata · IEEE Transactions on Software Engineering · 1990
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.>