A Petri-net-based correctness analysis of Internet stock trading systems

被引：29

作者：

Du, YuYue ^{[1
,2
]}

Jiang, ChangJun ^{[3
]}

Zhou, MengChu ^{[4
,5
]}

机构：

[1] Shandong Univ Sci & Technol, Coll Informat Sci & Engn, Qingdao 266510, Peoples R China

[2] Chinese Acad Sci, Comp Sci Lab, Inst Software, Beijing 100080, Peoples R China

[3] Tongji Univ, Dept Comp Sci & Engn, Shanghai 200092, Peoples R China

[4] New Jersey Inst Technol, Dept Elect Comp Engn, Newark, NJ 07102 USA

[5] Chinese Acad Sci, Inst Automat, Lab Complex Syst & Intelligence Sci, Beijing 100080, Peoples R China

来源：

IEEE TRANSACTIONS ON SYSTEMS MAN AND CYBERNETICS PART C-APPLICATIONS AND REVIEWS | 2008年 / 38卷 / 01期

基金：

中国国家自然科学基金;

关键词：

correctness; formal verification; Petri nets (PNs); stock trading systems; temporal logic;

D O I：

10.1109/TSMCC.2007.896995

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

This paper shows how temporal Petri nets (TPNs) can be used to specify and analyze an Internet stock trading system. The dynamical behavior of the system and causality between events can be explicitly described by temporal formulas. The functional correctness of the modeled system is formally verified by using the inferential rules in temporal logic. Important properties of the system are analyzed based on its TPN model such as liveness, eventuality, and fairness properties. This paper demonstrates that TPNs can provide significant advantages in the design and analysis of business processes.

引用

页码：93 / 99

页数：7

共 16 条

[1] Efficiency analysis of brokers in the electronic marketplace [J].

Almeida, VAF ;

Meira, W ;

Ribeiro, VF ;

Ziviani, N .

COMPUTER NETWORKS-THE INTERNATIONAL JOURNAL OF COMPUTER AND TELECOMMUNICATIONS NETWORKING, 1999, 31 (11-16) :1079-1090

[2] MODELING AND VERIFICATION OF TIME-DEPENDENT SYSTEMS USING TIME PETRI NETS [J].

BERTHOMIEU, B ;

DIAZ, M .

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1991, 17 (03) :259-273

[3]

CAMINADA MWA, P 5 INT WORKSH LANG, P107

[4]

CAMPBELL J, 2001, P 34 ANN HAW INT C S, V4, P4036

[5]

Du YY, 2003, LECT NOTES COMPUT SC, V2885, P452

[6] Binding telecooperation -: a formal model for electronic commerce [J].

Grimm, R ;

Ochsenschläger, P .

COMPUTER NETWORKS-THE INTERNATIONAL JOURNAL OF COMPUTER AND TELECOMMUNICATIONS NETWORKING, 2001, 37 (02) :171-193

[7]

KOUBARKIS M, 2000, P CAISE STOCKH SWED, P1

[8]

Lee RM, 1999, INT J ELECTRON COMM, V3, P105

[9] Timing constraint workflow nets for workflow analysis [J].

Li, JQ ;

Fan, YS ;

Zhou, MC .

IEEE TRANSACTIONS ON SYSTEMS MAN AND CYBERNETICS PART A-SYSTEMS AND HUMANS, 2003, 33 (02) :179-193

[10] An internet multicast system for the stock market [J].

Maxemchuk, NF ;

Shur, DH .

ACM TRANSACTIONS ON COMPUTER SYSTEMS, 2001, 19 (03) :384-412

← 1 2 →