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
基金
中国国家自然科学基金;
关键词
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 条
  • [11] Petri-Net-Based Analysis Method for Grid Services Composition Model
    Yu Xue-li
    Jiang Jing
    Xia Bai-qiang
    Pan Zhen-kuan
    [J]. 2010 INTERNATIONAL CONFERENCE ON INNOVATIVE COMPUTING AND COMMUNICATION AND 2010 ASIA-PACIFIC CONFERENCE ON INFORMATION TECHNOLOGY AND OCEAN ENGINEERING: CICC-ITOE 2010, PROCEEDINGS, 2010, : 180 - 184
  • [12] Petri-Net-Based Scheduling of Flexible Manufacturing Systems Using an Estimate Function
    Xu, Gongdan
    Chen, Yufeng
    [J]. SYMMETRY-BASEL, 2022, 14 (05):
  • [13] A Petri-Net-Based Virtual Deployment Testing Environment for Enterprise Software Systems
    Yu, Jian
    Han, Jun
    Schneider, Jean-Guy
    Hine, Cameron
    Versteeg, Steve
    [J]. COMPUTER JOURNAL, 2017, 60 (01): : 27 - 44
  • [14] Petri-Net-Based Model Checking for Privacy-Critical Multiagent Systems
    He, Leifeng
    Liu, Guanjun
    Zhou, Mengchu
    [J]. IEEE TRANSACTIONS ON COMPUTATIONAL SOCIAL SYSTEMS, 2023, 10 (02) : 563 - 576
  • [15] Compositional verification of concurrent systems using Petri-net-based condensation rules
    Juan, EYT
    Tsai, JJP
    Murata, T
    [J]. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1998, 20 (05): : 917 - 979
  • [16] Petri-net-based coordination algorithms for Grid transactions
    Tang, FL
    Li, ML
    Huang, JZX
    Wang, CL
    Luo, ZW
    [J]. PARALLEL AND DISTRIBUTED PROCESSING AND APPLICATIONS, PROCEEDINGS, 2004, 3358 : 499 - 508
  • [17] AgvSimNet: A Petri-Net-Based AGVS Simulation System
    S. Hsieh
    Y.-F. Chen
    [J]. The International Journal of Advanced Manufacturing Technology, 1999, 15 : 851 - 861
  • [18] Java']Java Software for Petri-Net-Based Approaches to Discrete Event Systems
    Wang, Xiaojun
    Han, Chun
    Hu, Hesuan
    [J]. 2018 IEEE 14TH INTERNATIONAL CONFERENCE ON CONTROL AND AUTOMATION (ICCA), 2018, : 330 - 335
  • [19] A Petri-net-based structure for AS/RS operation modelling
    Hsieh, S
    Hwang, JS
    Chou, HC
    [J]. INTERNATIONAL JOURNAL OF PRODUCTION RESEARCH, 1998, 36 (12) : 3323 - 3346
  • [20] A Colored Petri Net for Stock Trading Signal Detection
    Shih, Po-Yuan
    Shih, Dong-Her
    Liu, An-Chung
    [J]. 2016 IEEE CONGRESS ON EVOLUTIONARY COMPUTATION (CEC), 2016, : 4551 - 4554