Skip to main content
SpringerLink
Log in

A Formal Service Specification for the Internet Open Trading Protocol

  • Conference paper
  • First Online:
Application and Theory of Petri Nets 2002 (ICATPN 2002)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2360))

Included in the following conference series:

Abstract

This paper presents our service specification for the Internet Open Trading Protocol (IOTP) developed using Coloured Petri Nets. To handle IOTP’s complexity, we apply a protocol engineering methodology based on Open Systems Interconnection (OSI) principles consisting of five iterative steps: the definition of service primitives and parameters; the creation of an automaton specifying the local service language for each of the four trading roles of IOTP; the development of a CPN model synthesizing the local automata into a specification of the global service capturing the correlations between the service primitives at the distributed trading roles; the generation of the occurrence graph representing the global service language; and lastly a new step, language comparison to ensure the consistency between the specifications of the local service language and the global service language. The outcome is a proposed formal service specification for IOTP.

Partially supported by Australian Technology Network (ATN) Small Research Grant, 2001.

Supported by the Danish Natural Science Research Council.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. ITU-T Recommendation X.210, Information Technology-Open Systems Interaction-Basic Reference Model: Conventions For The Definition of OSI Services, November 1993.

    Google Scholar 

  2. ITU-T Recommendation X.214, Information Technology-Open Systems Interconnection-Transport Service Definition, November 1995.

    Google Scholar 

  3. AT&T. FSM Library. URL: http://www.research.att.com/sw/tools/fsm.

  4. J. Billington. Abstract Specification of the ISO Transport Service Definition using Labelled Numerical Petri Nets. In Protocol Specification, Testing, and Verification, III, pages 173–185. Elsevier Science Publishers, 1983.

    Google Scholar 

  5. J. Billington. Formal Specification of Protocols: Protocol Engineering. In Encyclopedia of Microcomputers, pages 299–314. Marcel Dekker, New York, 1991.

    Google Scholar 

  6. J. Billington, M. Diaz, and G. Rozenberg, editors. Application of Petri Nets to Communication Networks: Advances in Petri Nets, volume 1605 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, 1999.

    Google Scholar 

  7. J. Billington, M. C. Wilbur-Ham, and M. Y. Bearman. Automated Protocol Verification. In Protocol Specification, Testing, and Verification, V, pages 59–70. Elsevier Science Publishers, 1986.

    Google Scholar 

  8. D. Birch. Shopping Protocols-Buying online is more than just paying. Journal of Internet Banking and Commerce, 3(1), January 1998.

    Google Scholar 

  9. D. Burdett. Internet Open Trading Protocol-IOTP Version 1.0.IETF Trade Working Group, April 2000. IETF RFC 2801 URL: http://www.ietf.org/rfc/rfc2801.txt.

  10. D. Burdett, D. Eastlake, and M. Goncalves. Internet Open Trading Protocol. McGraw-Hill, 2000.

    Google Scholar 

  11. D. Eastlake and C. Smith. Internet Open Trading Protocol (IOTP) HTTP Supplement. IETF Trade Working Group, September 2000. IETF RFC 2935 URL: http://www.ietf.org/rfc/rfc2935.txt.

  12. S. Gordon and J. Billington. Modelling the WAP Transaction Service using Coloured Petri Nets. In Proceedings of MDA 1999, LNCS 1748, pages 105–114. Springer-Verlag, 1999.

    Google Scholar 

  13. InterPay I-OTP. URL: ftp://ftp.pothole.com/pub/ietf-trade/IETF-London/InterPay2001London.ppt%

  14. The Internet Engineering Task Force-IETF. URL: http://www.ietf.org/.

  15. JOTP Open Trading Protocol Toolkit For Java. URL: http://www.livebiz.com/.

  16. K. Jensen. Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use. Vol 1-3 Monographs in Theoretical Computer Science. Springer-Verlag, 1997.

    Google Scholar 

  17. G. C. Kessler and N. T. Pritsky. Payment protocols: Cache on demand. Information Security Magazine, October 2000. Availabe via http://www.infosecuritymag.com/articles/october00/features2.shtml.

  18. H. R. Lewis and C. H. Papadimitriou. Elements of the Theory of Computation. Prentice-Hall International, 1998.

    Google Scholar 

  19. Mondex. URL: http://www.mondexusa.com/html/content/technolo/technolo.htm.

  20. Design/CPN Online. URL: http://www.daimi.au.dk/designCPN/.

  21. 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, Department of Computer Science, University of Aarhus, ISSN 0105-8517, 2001.

    Google Scholar 

  22. C. Ouyang, L. M. Kristensen, and J. Billington. A Proposed Internet Open Trading Service Definition. Technical report, Computer Systems Engineering Centre, University of South Australia, 2001. Draft version 2.0.

    Google Scholar 

  23. C. Ouyang, L. M. Kristensen, and J. Billington. Towards Modelling and Analysis of the Internet Open Trading Protocol Transactions using Coloured Petri Nets. In Proceedings of 11th Annual International Symposium of the International Council on System Engineering (INCOSE), pages CD-ROM 6.7.3, 2001.

    Google Scholar 

  24. 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.

    Google Scholar 

  25. W. Reisig and G. Rozenberg, editors. Lectures on Petri Nets: Advances in Petri Nets. Volume I: Basic Models, volume 1491 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, 1998.

    Google Scholar 

  26. Hitachi SMILEs. URL: http://www.hitachi.co.jp/Div/nfs/whats_new/smiles.html.

  27. M. E. Villapol and J. Billington. Generation of a Service Language for the Resource Reservation Protocol Using Formal Methods. In Proceedings of 11th Annual International Symposium of the International Council on Systems Engineering (IN-COSE), pages CD–ROM 9.1.4, 2001.

    Google Scholar 

  28. Visa and MasterCard. SET Secure Electronic Transaction Specification. Version 1.0. Vol 1–3, May 1997. URL: http://www.setco.org/set_specifications.html.

Download references

Author information

Authors and Affiliations

  1. Computer Systems Engineering Centre School of Electrical and Information Engineering, University of South Australia, Mawson Lakes Campus, SA, 5095, Australia

    Chun Ouyang, Lars Michael Kristensen & Jonathan Billington

Authors
  1. Chun Ouyang
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Lars Michael Kristensen
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Jonathan Billington
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Division of Informatics, University of Edinburgh, James Clerk Maxwell Building, The King’s Buildings Mayfield Road, Edinburgh, EH9 3JZ, UK

    Javier Esparza

  2. Department of Computer Science, University of Adelaide, North Terrace, Adelaide, SA, 5005, Australia

    Charles Lakos

Rights and permissions

Reprints 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 Service Specification for the Internet Open Trading Protocol. In: Esparza, J., Lakos, C. (eds) Application and Theory of Petri Nets 2002. ICATPN 2002. Lecture Notes in Computer Science, vol 2360. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48068-4_21

Download citation

  • DOI: https://doi.org/10.1007/3-540-48068-4_21

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-43787-1

  • Online ISBN: 978-3-540-48068-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation