Abstract
The Internet Open Trading Protocol (IOTP) is being developed by the Internet Engineering Task Force for electronic commerce (e-commerce) over the Internet. The core of IOTP is a set of trading transactions that reflects the most common trading activities in the real world. We apply the formal method of Coloured Petri Nets (CP-nets) to construct an abstract executable specification of IOTP’s trading transaction protocols. The formal semantics of CP-nets allows us to investigate the termination properties of the transactions using state space techniques. This investigation has revealed deficiencies in the termination of IOTP trading transactions, demonstrating the benefit of applying formal methods to the specification and verification of e-commerce protocols.
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
J. Billington, M. Diaz, and G. Rozenberg, editors. Application of Petri Nets to Communication Networks: Advances in Petri Nets, Volume 1605, Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1999.
D. Burdett. Internet Open Trading Protocol IOTP Version 1.0. IETF Trade Working Group, April 2000. Available via: http://www.ietf.org/rfc/rfc2801.txt.
E. Clarke, O. Grumberg, and D. Peled. Model Checking. The MIT Press, 1999.
E. M. Clarke and J.M Wing. Formal Methods: State of the Art and Future Directions. ACM Computing Surveys, 28(4):626–643, December 1996.
K. Jensen. Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use. Vol 1–3. Monographs in Theoretical Computer Science. Springer-Verlag, 1997.
L.M. Kristensen, S. Christensen, and K. Jensen. The Practitioner’s Guide to Coloured Petri Nets. International Journal on Software Tools for Technology Transfer, 2(2):98–132, 1998. Springer-Verlag.
R.M. Lee. Documentary Petri Nets: A Modelling Representation for Electronic Trade Procedure. In Business Process Management, Volume 1806, Lecture Notes in Computer Science, pages 259–375. Springer-Verlag, 2000.
C. Ouyang, L.M. Kristensen, and J. Billington. An Improved Architectural Specification of the Internet Open Trading Protocol. In Proceedings of 3rd Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools (CPN’01), pages 119–137. DAIMI PB-554, University of Aarhus, ISSN 0105-8517, 2001.
C. Ouyang, L.M. Kristensen, and J. Billington. Towards Modelling and Analysis of the Internet Open Trading Protocol Transactions using Coloured Petri Nets. In Proc of 11th Annual International Symposium of the International Council on System Engineering (INCOSE), 2001. CD-ROM 6.7.3.
C. Ouyang, L.M. Kristensen, and J. Billington. A Formal Service Specification of the Internet Open Trading Protocol. In Proceedings of 23rd International Conference on Application and Theory of Petri Nets, Volume 2360, Lecture Notes in Computer Science, Springer-Verlag, 2002. To appear.
M. Papa, O. Bremer, J. Hale, and S. Shenoi. Formal Analysis of E-commerce Protocols. In Proceedings of 5th. International Symposium on Autonomous Decentralized Systems, pages 19–28. IEEE Computer Society, 2001.
I. Ray and I. Ray. Failure Analysis of an E-commerce Protocol using Model Checking. In Proceedings of 2nd International Workshop on Advanced Issues of ECommerce and Web-Based Information Systems, pages 176–183. IEEE Computer Society, 2000.
W. Reisig and G. Rozenberg, editors. Lectures on Petri Nets: Advances in Petri Nets. Volume I: Basic Models, Volume 1491, Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1998.
J. D. Ullman. Elements of ML Programming. Prentice-Hall, 1998.
P. Yolum and M. P. Singh. Commitment-based enhancement of e-commerce protocols. In Proceedings of IEEE 9th International Workshops on Enabling Technologies: Infrastructure for Collaborative Enterprises, pages 278–283, 2000.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ouyang, C., Kristensen, L.M., Billington, J. (2002). A Formal and Executable Specification of the Internet Open Trading Protocol. In: Bauknecht, K., Tjoa, A.M., Quirchmayr, G. (eds) E-Commerce and Web Technologies. EC-Web 2002. Lecture Notes in Computer Science, vol 2455. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45705-4_39
Download citation
DOI: https://doi.org/10.1007/3-540-45705-4_39
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-44137-3
Online ISBN: 978-3-540-45705-3
eBook Packages: Springer Book Archive