Correctness Verification of E-Commerce Taxation Systems Using Mobile-Agent-Oriented Petri Nets

Author

Gan, Zaobin ; He, Juxia ; Yang, Xiao

Author_Institution

Coll. of Comput. Sci. & Tech., Huazhong Univ. of Sci. & Tech., Wuhan, China

fYear

2009

fDate

26-28 Dec. 2009

Firstpage

2893

Lastpage

2896

Abstract

This paper shows how Mobile-Agent-oriented Petri nets (MAPNs) can be used to specify and analyze a mobile-agent-based e-commerce taxation system. Both the dynamical behavior of the system and the causality between events can be explicitly described by MAPNs. The functional correctness of the system, such as the reachability and the coverability, is formally verified by attaching agents´ attributes to the tokens of the classical Petri nets. The application instance in this paper demonstrates that MAPNs can provide more information and be more helpful in the design and analysis of business processes based on mobile agents.

Keywords

Petri nets; electronic commerce; formal verification; mobile agents; taxation; Petri nets; business process analysis; correctness verification; e-commerce taxation systems; mobile agent; Application specific processors; Bars; Educational institutions; Gallium nitride; Helium; Information analysis; Information science; Joining processes; Mobile agents; Petri nets;

fLanguage

English

Publisher

ieee

Conference_Titel

Information Science and Engineering (ICISE), 2009 1st International Conference on

Conference_Location

Nanjing

Print_ISBN

978-1-4244-4909-5

Type

conf

DOI

10.1109/ICISE.2009.437

Filename

5454924