Formal design of online ticketing system in uml

UNU/IIST
International Institute for Software Technology

A Formal Design of Online Ticketing System in UML
Xiaoshan Li, Zhiming Liu and Zhengshen Guo
July 2001

UNU/IIST Report No. 235

 

UNU/IIST and UNU/IIST Reports
UNU/IIST (United Nations University International Institute for Software Technology) is a Research and Training Centre of the United Nations University (UNU). It isbased in Macau, and was founded in 1991. It started operations in July 1992. UNU/IIST is jointly funded by the Governor of Macau and the governments of the People’s Republic of China and Portugal through a contribution to the UNU Endownment Fund. As well as providing twothirds of the endownment fund, the Macau authorities also supply UNU/IIST with its office premises and furniture and subsidisefellow accommodation. The mission of UNU/IIST is to assist developing countries in the application and development of software technology. UNU/IIST contributes through its programmatic activities: 1. Advanced development projects, in which software techniques supported by tools are applied, 2. Research projects, in which new techniques for software development are investigated, 3. Curriculumdevelopment projects, in which courses of software technology for universities in developing countries are developed, 4. University development projects, which complement the curriculum development projects by aiming to strengthen all aspects of computer science teaching in universities in developing countries, 5. Courses, which typically teach advanced software development techniques, 6. Events, in whichconferences and workshops are organised or supported by UNU/IIST, and 7. Dissemination, in which UNU/IIST regularly distributes to developing countries information on international progress of software technology. Fellows, who are young scientists and engineers from developing countries, are invited to actively participate in all these projects. By doing the projects they are trained. At present,the technical focus of UNU/IIST is on formal methods for software development. UNU/IIST is an internationally recognised center in the area of formal methods. However, no software technique is universally applicable. We are prepared to choose complementary techniques for our projects, if necessary. UNU/IIST produces a report series. Reports are either Research R , Technical T , Compendia C orAdministrative A . They are records of UNU/IIST activities and research and development achievements. Many of the reports are also published in conference proceedings and journals. Please write to UNU/IIST at P.O. Box 3058, Macau or visit UNU/IIST home page: http://www.iist.unu.edu, if you would like to know more about UNU/IIST and its report series.

Zhou Chaochen, Director — 01.8.1997 – 31.7.2001UNU/IIST
International Institute for Software Technology

P.O. Box 3058 Macau

A Formal Design of Online Ticketing System in UML
Xiaoshan Li, Zhiming Liu and Zhengshen Guo

Abstract
E-commerce systems have been changing the traditional business activities through the Internet. An ecommerce system can be seen as a client-server system in which a server maintains some information andprovides 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. Using an online ticketing system as a case study, this paper presents a formal use of the Unified Modelling Language (UML) to the analysis and design of e-commerce systems. We demonstrate how the formalization given in[13,14] can be used in formal specification of the system functional requirements, safety and liveness constraints, and in verification of the correctness of the design. Keywords: UML, E-Commerce, Formal Techniques, safety, Liveness, Object-Orientation.

Xiaoshan Li is an Assistant Professor at the University of Macau. His research areas are Interval Temporal Logic, formal specification,...