In: K. Bauknecht, A. Min Tjoa, G. Quirchmayr (Eds.): E-Commerce and Web Technologies, Third International Conference (EC-Web 2002), Aix-en-Provence, France, September 2-6, 2002, pages 1-377pp. Springer Verlag, LNCS 2455, August 2002.
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.