A Formal Approach for Obligation Analysis of E-Commerce  

作　　者：DU Yuyue JIANG Changjun 

机构地区：[1]College of Information Science and Engineering, Shandong University of Science and Technology, Qingdao 266510, China [2]Department of Computer Science and Engineering, Tongji University, Shanghai 200092, China [3]The State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing 100080, China

出　　处：《Chinese Journal of Electronics》2008年第2期200-204,共5页电子学报（英文版）

摘　　要：Existing methods for modeling Ecommerce systems （ECSs） focus mostly on either mathematically abstract verification or graphical modeling, and cannot explicitly describe and analyze the obligations of partners. This work presents a new class of Labeled Petri nets for the modeling and analysis of ECSs. And the life cycle of a case and the time/date of firing an action are considered. It can model graphically the dynamic behavior of the systems, and analyze elegantly the obligations. This approach is illustrated with a nontrivial example of the modeling and analysis of the trading process of the Purchase transaction in the Internet open trading protocol.

关 键 词：Frcommerce system Labeled Petri net Formal modeling VERIFICATION Obligation analysis. 

分 类 号：F713.36[经济管理—产业经济]