In: Nielsen, M.; Simpson, D.: Lecture Notes in Computer Science, Vol. 1825: 21st International Conference on Application and Theory of Petri Nets (ICATPN 2000), Aarhus, Denmark, June 2000, pages 207-226. Springer-Verlag, 2000.
Abstract: Coloured Petri nets (CPNs) are used to specify and analyse the Class 2 Wireless Transaction Protocol (WTP). The protocol provides a reliable request/response service to the Session layer in the Wireless Application Protocol (WAP) architecture. When only a single transaction is considered occurrence graph and language analysis reveals 3 inconsistencies between the protocol and service specification: the initiator user can receive two invoke primitives; turning user acknowledgment on doesn't always provide the user acknowledgment service; and a transaction can be aborted without the responder user being notified. Based on the modelling and analysis, changes to WTP have been recommended to the WAP Forum.