Modeling And Analysis Of WAP Transaction Layer Protocol Using Colored Petri Net

The Transaction layer, as an important part in WAP, defines a protocol to support distributed transactions where an Initiator makes a request to a Responder, which returns the requested information. As the specification of WAP protocol was written in natural language, the advantage of doing it in this way is well readable and easy to understand. However, to guarantee the correctness and conformance of protocol implementation, a formal technique must be used to avoid the ambiguity of natural language.Petri net, as a mathematic modeling technique, is especially suitable for modeling distributed dispersed system with the characteristic of concurrency real-time and nondeterminacy. Also, it has many analytical methods which can determine whether the model has a dead lock, conflict of concurrency and competition of resource. Colored Petri net, as an advanced net, enrich the ability of expression of place and transition. So it can simplify the structure of the model.In this thesis, the state change of protocol entity is modeled by Colored Petri Net in a transaction, which is based on the analysis of WTP protocol specification. Finally, the CPN model of transaction protocol is simulated by CPN tools under the initial parameter. The results obtained from the simulation can be used to determine whether there is a dead lock or live lock in the model and the boundedness of the model, observations are made on the relationship between the counters used in the model and the state space size.