Petri nets for protocol engineering

This paper presents a review of the role Petri nets play in protocol engineering. This methodology provides various models for specification and many methods for verification and other software engineering tasks concerning protocols. In particular, many property-preserving transformations and compositional methods are available for reducing the impact of state explosion on the two well-known verification approaches - reachability analysis and invariant analysis. By conversion, Petri nets can be used for studying systems specified by many of the formal description techniques frequently used for protocol investigation such as MSG, SDL, ESTELLE, LOTOS, CCS, CSP and CCSP. For example, Petri nets can be used for deriving test sequences and cyclomatic complexity measure for LOTOS. Also, many equivalence relations concerning the theoretical foundation of protocol engineering have been formulated on the basis of Petri nets. Other developments of Petri nets related to protocols include: Petri nets with temporal logic, feature interaction, synthesis, complexity measure, timed or object-related Petri nets, etc.