In: 11th Annual International Symposium of the International Council on Systems Engineering (INCOSE 2001), pages 1-8 pgs. 1-5 July 2001. Melbourne, Australia.
Abstract: Electronic Commerce (E-Commerce) is a rapidly growing area with new companies entering the market place and existing companies moving their commercial operations onto the Internet. The Internet Open Trading Protocol (OTP) is a standard being developed by the Internet Engineering Task Force aiming at providing an interoperable framework for E-Commerce over the Internet. In this paper we use Coloured Petri Nets (CP-nets or CPNs) to construct an executable model of the IOTP Deposit Transaction. Due to the formal semantics of CP-nets, this CPN model constitutes an unambiguous specification of the Deposit Transaction and allows us to conduct a formal analysis of the Deposit Transaction. This initial analysis has already revealed minor deficiencies in the Deposit Transaction procedures demonstrating the benefit of applying formal methods for the specification and development of complex communication protocols.