In: E-Commerce: FORTE 2004 Workshops The FormEMC, EPEW, ITM, Toledo, Spain, October 1-2, 2004: Proceedings of Applying Formal Methods: Testing, Performance, and M, pages 1-15. Volume 3236 of Lecture Notes in Computer Science / Manuel Núñez, Zakaria Maamar, Fernando L. Pelayo et al. (Eds.) --- Springer-Verlag, September 2004.
Abstract: The Internet Open Trading Protocol (IOTP) is an electronic commerce (e-commerce) protocol developed by the Internet Engineering Task Force (IETF) to support online trading activities. The core of IOTP is a set of financial transactions and therefore it is vitally important that the protocol operates correctly. An informal specification of IOTP is published as Request For Comments (RFC) 2801. We have applied the formal method of Coloured Petri Nets (CPNs) to obtain a formal specification of IOTP. Based on the IOTP CPN specification, this paper presents a detailed investigation of a set of behavioural properties of IOTP using state space techniques. The analysis reveals deficiencies in the termination of IOTP transactions, demonstrating the benefit of applying formal methods to the specification and verification of e-commerce protocols.