摘要

Electronic commerce (E-commerce) is an important Internet application that is significantly changing the way of commercial transaction. Due to the complexity of E-commerce systems and lack of well-designed formal models, providing a suitable method for their modeling and monitoring turns but to be a challenging job. This paper introduces labeled workflow nets (LWN) and their semantics on the basis of labeled Petri nets. Then an inter-organizational labeled workflow net (ILWN) - which can graphically model the dynamic behavior of the systems - is presented. Furthermore, the nonblocking property of ILWNS is defined to achieve a common goal of E-commerce participants. This nonblocking property helps to analyze the soundness of ILWNs and the undeniable property of interactive actions. The proposed framework for E-commerce workflows (ECW) can record a history of interactive events and monitor the execution of interactive activities to achieve a common goal. Therefore, it can elegantly model the execution of interorganizational workflows and analyze the accountability of cooperative activities. The main contribution of the paper is to present a new formal mechanism - ILWN. It can efficiently support the modeling and monitoring of ECWs. Finally, this paper illustrates how to use the proposed method by modeling and analyzing a Customer-Producer-Supplier example.