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: (1) the initiator user can receive two TR-Invoke.cnf primitives; (2) turning User Acknowledgement on doesn’t always provide the User Acknowledgement service; and (3) 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 ForumSM.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
W. A. Barret and J. D. Couch. Compiler Construction: Theory and Practice. Science Research Associates, 1979.
M. Y. Bearman, M. C. Wilbur-Ham, and J. Billington. Specification and analysis of the OSI Class 0 Transport Protocol. In J. M. Bennet and P. Pearcey, editors, Proc. of the 7th Int. Conf. on Computer Communications, pages 602–607, Sydney, Australia, 30 Oct.–2 Nov. 1984. North Holland Publishers.
J. Billington. Formal specification of protocols: Protocol engineering. In Encyclopedia of Microcomputers, pages 299–314. Marcel Dekker, New York, NY, 1991.
J. Billington, M. Diaz, and G. Rozenberg, editors. Application of Petri Nets to Communication Networks: Advances in Petri Nets. LNCS 1605. Springer-Verlag, Berlin, 1999.
R. Braden. T/TCP-TCP extensions for transactions functional specification. IETF RFC 1644 URL: ftp://ftp.isi.edu/in-notes/rfc1644.txt, July 1994.
S. Budkowski, B. Alkechi, M. L. Benalycherif, P. Dembinski, M. Gardie, E. Lallet, J. P. Mouchel La Fusse, and Y. Soussi. Formal specification, validation and perfor mance evaluation of the Xpress Transfer Protocol. In A. Danthine, G. Leduc, and P. Wolper, editors, Protocol Specification, Testing and Verification, XIII, pages 191–206, Liege, Belgium, May 1993.
B. Cheong and S. Gordon. Automata Reduction Tool (ART): System Manual. Institute for Telecommunications Research, University of South Australia, 25 February 1999.
J. C. A. de Figueiredo and L. M. Kristensen. Using Coloured Petri nets to investigate behavioural and performance issues of TCP protocols. In K. Jensen, editor, Proc. of the 2nd Workshop on the Practical Use of Coloured Petri Nets and Design/CPN, pages 21–40, Aarhus, Denmark, 13–15 October 1999. Department of Computer Science, Aarhus University. PB-541.
S. Gordon and J. Billington. Modelling and analysis of the WAP class 2 Wireless Transaction Protocol using Coloured Petri nets. Draft technical report, Institute for Telecommunications Research, University of South Australia, Adelaide, Australia, November 1999.
S. Gordon and J. Billington. WAP Forum Input Document: Inconsistencies in the Wireless Transaction Protocol. Submitted to WAP Forum 19 November 1999.
S. Gordon and J. Billington. Modelling the WAP Transaction Service using Coloured Petri nets. In H.-V. Leong, W.-C. Lee, B. Li, and L. Yin, editors, Proc. of the 1st Int. Conf. on Mobile Data Access, LNCS 1748, pages 109–118, Hong Kong, 16–17 December 1999. Springer-Verlag.
ITU. Information Technology-OSI-Basic reference model: The basic model. ITU-T Recommendation X.200 ∣ ISO/IEC 7498, July 1994.
ITU. Information Technology-OSI-Protocol for providing the connection-mode transport service. ITU-T Recommendation X.224 ∣ ISO/IEC 8073, November 1995.
K. Jensen. Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use, volume 1, Basic Concepts, Monographs in Theoretical Computer Science. Springer-Verlag, Berlin, 1997.
K. Jensen. Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use, volume 3, Practical Use, Monographs in Theoretical Computer Science. Springer-Verlag, Berlin, 1997.
G. M. Lundy and R. C. McArthur. Formal model of a high speed transport protocol. In R. J. Linn and M. U. Uyar, editors, Protocol Specification, Testing and Verification, XII, pages 97–111, Lake Buena Vista, FL, June 1992.
H. Mehrpour and A. E. Karbowiak. Modelling and analysis of DOD TCP/IP protocol using numerical Petri nets. In Proc. of IEEE Region 10 Conf. on Computer Communication Systems, pages 617–622, Hong Kong, September 1990.
Meta Software Corporation. Design/CPN Reference Manual for X-Windows, Version 2.0. Meta Software Corporation, Cambridge, MA, 1993.
J. Postel. User Datagram Protocol. IETF RFC 768 URL: ftp://ftp.isi.edu/in-notes/rfc768.txt, August 1980.
J. Postel. Transmission Control Protocol. DARPA Internet program protocol specification. Information Sciences Institute, University of Southern California, Marina del Ray, CA, September 1981. IETF RFC 793 URL: ftp://ftp.isi.edu/in-notes/rfc793.txt.
D. Raymond and D. Wood. User’s Guide to Grail. Dept. of Computer Science, University of Western Ontario, London, Canada, March 1996. Version 2.5.
M. A. Smith. Formal verification of communication protocols. In R. Gotzhein and J. Bredereke, editors, Formal Description Techniques IX: Theory, Applications, and Tools, pages 129–144. Chapman & Hall, London, UK, October 1996.
M. A. Smith. Reliable message delivery and conditionally-fast transactions are not possible without accurate clocks. In Proc. of the 17th Annual ACM Symposium on Principles of Distributed Computing, Puerto Vallarto, Mexico, June 1998.
WAP Forum. Wireless Application Protocol Architecture Specification. Available via http://www.wapforum.org/, 30 April 1998.
WAP Forum. Wireless Application Protocol Wireless Transaction Protocol Specification. Available via http://www.wapforum.org/, 11 June 1999.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gordon, S., Billington, J. (2000). Analysing the WAP Class 2 Wireless Transaction Protocol Using Coloured Petri Nets. In: Nielsen, M., Simpson, D. (eds) Application and Theory of Petri Nets 2000. ICATPN 2000. Lecture Notes in Computer Science, vol 1825. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44988-4_13
Download citation
DOI: https://doi.org/10.1007/3-540-44988-4_13
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67693-5
Online ISBN: 978-3-540-44988-1
eBook Packages: Springer Book Archive