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

Yu Yue Du, Chang Jun Jiang, Meng Chu Zhou

Research output: Contribution to journalArticlepeer-review

44 Scopus citations


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 languageEnglish (US)
Pages (from-to)93-99
Number of pages7
JournalIEEE Transactions on Systems, Man and Cybernetics Part C: Applications and Reviews
Issue number1
StatePublished - Jan 2008
Externally publishedYes

All Science Journal Classification (ASJC) codes

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


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


Dive into the research topics of 'A Petri-Net-Based Correctness Analysis of Internet Stock Trading Systems'. Together they form a unique fingerprint.

Cite this