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
相关论文
共 50 条
12345