Petri Nets Theory for the Correctness of Protocols

After a brief introduction to the theory of Petri nets, the ECMA transport protocol is presented. Then a model of the connection and disconnection phases is developed. Properties of correctness are demonstrated, using Petri net theory results, namely, reductions and linear invariants techniques. Predicate/transition nets are introduced and the underlying network service is modeled. Then a model of the data transfer phase is described. It allows correction of the errors signaled by the network level, by using a window mechanism and control frames for acknowledgments and rejections. The correctness of the data transfer is demonstrated using invariants. The service provided to the upper level is thus validated.