Study Of Specification And Verification Of Protocols Based On Extended Time Petri Nets

A protocol is crucial in computer network. The improvement of the complexity of a protocol brings on protocol engineering discipline. The main activities of protocol engineering consist of the protocol specification, verification, performance evaluation, automatic implementation and conformance testing. The protocol specification and analysis are very important steps of activities in protocol engineering, and they are basic steps of other activities in protocol engineering. The thesis summarizes the advantages of adopting Petri net as the tool of protocol specification and analysis on the foundation of reviewing three kinds of relatively existing formal description techniques (FDTs). For the better extension simulative ability of Time Petri nets and the convenience of modeling a protocol, Inhibitor arcs are added to realize another kind of control to the firing of transition on the foundation of Time Petri nets defined by Merlin. We propose Time Petri nets with Inhibitor arcs (shortened form ETPN), and define the states of ETPN, enabledness and firability conditions of transition and firing rules of transition. On the foundation of analyzing to the net system, we improve traditional reachability analysis technique, and use Time Petri nets with Inhibitor arcs to model IEEE 802.2 LLC 3 type protocol. Three necessary conditions on the parameters are derived, and then a reduced reachability graph is obtained by applying the necessary conditions to lessen the combinatorial state explosion. And these dynamic characteristics to this model are verified preliminarily using the reduced reachability graph.