A Petri-Net-Based Correctness Analysis of Internet Stock Trading Systems

Yu Yue Du; Chang Jun Jiang; Meng Chu Zhou

doi:10.1109/TSMCC.2007.896995

A Petri-Net-Based Correctness Analysis of Internet Stock Trading Systems

Yu Yue Du, Chang Jun Jiang, Meng Chu Zhou

Research output: Contribution to journal › Article › peer-review

44 Scopus citations

Abstract

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.

Original language	English (US)
Pages (from-to)	93-99
Number of pages	7
Journal	IEEE Transactions on Systems, Man and Cybernetics Part C: Applications and Reviews
Volume	38
Issue number	1
DOIs	https://doi.org/10.1109/TSMCC.2007.896995
State	Published - Jan 2008
Externally published	Yes

All Science Journal Classification (ASJC) codes

Control and Systems Engineering
Software
Information Systems
Human-Computer Interaction
Computer Science Applications
Electrical and Electronic Engineering

Keywords

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

Access to Document

10.1109/TSMCC.2007.896995

Cite this

@article{6e11e906d4834f5ba49569bcbc95e2ee,

title = "A Petri-Net-Based Correctness Analysis of Internet Stock Trading Systems",

abstract = "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.",

keywords = "Correctness formal, stock trading systems, temporal logic, verification Petri nets (PNs)",

author = "Du, {Yu Yue} and Jiang, {Chang Jun} and Zhou, {Meng Chu}",

note = "Funding Information: Manuscript received January 9, 2005; revised June 29, 2005. This work was supported in part by the “Taishan Scholar” Construction Project of Shandong Province, China, in part by the National Natural Science Foundation of China under Grant 60573018, in part by the National Basic Research Program of China (973 Program) under Grant 2003CB316902 and Grant 2004CB318001-03, and in part by an open project of the Laboratory of Computer Science, Institute of Software, Chinese Academy of Science under Grant SYSKF0604. This paper was recommended by Associate Editor M. D. Jeng.",

year = "2008",

month = jan,

doi = "10.1109/TSMCC.2007.896995",

language = "English (US)",

volume = "38",

pages = "93--99",

journal = "IEEE Transactions on Systems, Man and Cybernetics Part C: Applications and Reviews",

issn = "1094-6977",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

number = "1",

}

TY - JOUR

T1 - A Petri-Net-Based Correctness Analysis of Internet Stock Trading Systems

AU - Du, Yu Yue

AU - Jiang, Chang Jun

AU - Zhou, Meng Chu

N1 - Funding Information: Manuscript received January 9, 2005; revised June 29, 2005. This work was supported in part by the “Taishan Scholar” Construction Project of Shandong Province, China, in part by the National Natural Science Foundation of China under Grant 60573018, in part by the National Basic Research Program of China (973 Program) under Grant 2003CB316902 and Grant 2004CB318001-03, and in part by an open project of the Laboratory of Computer Science, Institute of Software, Chinese Academy of Science under Grant SYSKF0604. This paper was recommended by Associate Editor M. D. Jeng.

PY - 2008/1

Y1 - 2008/1

N2 - 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.

AB - 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.

KW - Correctness formal

KW - stock trading systems

KW - temporal logic

KW - verification Petri nets (PNs)

UR - http://www.scopus.com/inward/record.url?scp=85008048565&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85008048565&partnerID=8YFLogxK

U2 - 10.1109/TSMCC.2007.896995

DO - 10.1109/TSMCC.2007.896995

M3 - Article

AN - SCOPUS:85008048565

SN - 1094-6977

VL - 38

SP - 93

EP - 99

JO - IEEE Transactions on Systems, Man and Cybernetics Part C: Applications and Reviews

JF - IEEE Transactions on Systems, Man and Cybernetics Part C: Applications and Reviews

IS - 1

ER -

A Petri-Net-Based Correctness Analysis of Internet Stock Trading Systems

Abstract

All Science Journal Classification (ASJC) codes

Keywords

Access to Document

Other files and links

Fingerprint

Cite this