Verification of Communication Protocols Using Petri Nets

Anisimov N.A. Postupalski P.A.

In: Mathematical Transactions, Vol.5, pp.24-42, Dalnauka (Vladivostok, 1996), In Russian.

Abstract

This paper addresses the problem of protocol verification as demonstration of the correspondence between the protocol and provided service. As a formal basis we use Petri nets. For specification of protocol entities, services, models of protocol layers we suggest to employ previously introduced model called Petri net entity. The Petri net entity is defined to be a Petri net equipped with a set of labelling called access points. We also use compositionof entities and a notion of entity equivalence that is based on a step bisimulation (SB-) equivalence between two labelled Petri nets. The problem of protocol verification is shown to be reduced to the problem of checking two labelled Petri nets for SB-equivalence. We suggest two-steps scheme of the checking. At the first step we build step reachability graph for both nets based on a classical algorithm of building a Petri net coverability tree. However, here we take into consideration firing of steps of transition rather then single ones. At the second step these two reachability graphs are transformed into two transition systems for which we employ the Kanellakis-Smolka algorithm for checking these systems for SB-equivalence. It is proven that this approach does allow one to check two Petri nets for step SB-equivalence. At the same time we show that SB-equivalence is to discriminative for protocol verification. The point is that it takes into consideration steps transitions which are distributed in space and will not simultaneously affect on local entity. To weaken the equivalence we partition a set of transition onto distributed sets and build reduced a reachability graph for each Petri net. Such procedure gives us distributed SB-equivalence. This approach is implemented within the framework of a Petri net tool called PN3-Editor. Some characteristics of the implementation are presented.