E-commerce systems have been changing the 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 by 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 transaction. We demonstrate how to use the formalization of UML given in [9, 10] in formal specification of the system functional requirements, safety and liveness constraints, and in verification of the correctness of the design.