Formal object-oriented analysis and design of an online ticketing system

E-commerce systems have been changing traditional business activities through the Internet. This paper presents a formal use of the Unified Modeling Language (UML) to analyze and design e-commerce systems using an online ticketing system as a case study. An e-commerce system can be seen as a client-server system in which a server maintains some information and provides a searching function to a client. However, for an e-commerce system we also need to consider two specific functions for booking products and carrying out payment transactions. We demonstrate how to use the formalization of UML given by Xiaoshan et al. (2001) in formal specification of the system functional requirements, safety and liveness constraints, and in verification of the correctness of the design.