25th Annual International Computer Software and Applications Conference. COMPSAC 2001 (2001)
Oct. 8, 2001 to Oct. 12, 2001
Wei Jun , Hong Kong University of Science and Technology
Cheung Shing-chi , Hong Kong University of Science and Technology
Wang Xu , Hong Kong University of Science and Technology
While e-commerce continuously grows prosperous, some advantages e-commerce applications claimed haven't really been gained. More seriously, the availability and reliability of these systems are particularly hard to obtain. The e-commerce protocols, as the core of e-commerce applications, ask for new development approach and techniques to be introduced for their highly reliable and safe design and implementation. This paper describes research on synthesis of extended UML formalism and formal verification techniques for automatic development of e-commerce protocols. In this paper, we refine AUML protocol diagrams for visual modeling, and develop algorithm and rules to translate visually modeled e-commerce protocols into formal models that are then validated using model checking. This approach is applied to the design of an e-commerce protocol -NetBill as exemplification. Our objective is to create tools that enable designers to automatically develop available and reliable e-commerce protocols.
Agent UML, UML, e-commerce protocol, Spin/Promela, model checking, formal methods
W. Jun, W. Xu and C. Shing-chi, "Exploiting Automatic Analysis of E-Commerce Protocols," 25th Annual International Computer Software and Applications Conference. COMPSAC 2001(COMPSAC), Chicago, Illinois, 2001, pp. 55.