In: Lecture Notes in Computer Science, Vol. 2455, Proc 3rd International Conference, EC-Web 2002, pages pp.377-387. 2-6 September 2002. Aix-en-Provence, France, Springer Verlag.
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.