As the mobile agent technology begins to emerge as a viable solution for intelligent e-commerce applications, there is an increasing attempt to ensure that the systems being developed are robust, reliable and manageable. While the mobile-agent-based e-commerce systems are desgined and implemented, their functional correctness and completeness must be formally verified. For this purpose, this paper introduces an extension of Petri nets, mobile-agent-oriented Petri nets (MAPN), for modeling and analyzing transaction workflows in mobile-agent-based e-commerce systems. By attaching some attributes to the tokens of the classical Petri nets, every token can be regarded as an agent to roam around the places to excutive certain tasks. In order to illustrate our formal model (MAPN) is effective for mobile agents modeling in e-commerce systems, an example of product search between buyers and sellers is provided. Meanwhile, the reachability and the coverability of the model are analyzed as well. Compared with exsiting formal description of agent-based systems, the tokens in MAPN model can carry more information, make the model more simple and powerful.
展开▼
