Title :
Formal analysis of an online stock trading system by temporal Petri nets
Author :
Du, Y.Y. ; Jiang, C.J.
Author_Institution :
Dept. of Comput. Sci. & Eng., Tongji Univ., Shanghai, China
Abstract :
Temporal Petri nets greatly enhance the modeling and analyzing power of Petri nets. The dynamic behavior of a given system and causality in events can be elegantly described by formulas containing temporal operators. We show how temporal Petri nets can be used for formal specification and verification of an online stock trading system. The functional correctness of the modeled system is formally analyzed by using the inference rules of temporal logic. Certain important properties of the temporal Petri net model are given. Finally; the further studying subjects are represented
Keywords :
Petri nets; discrete event systems; financial data processing; formal specification; real-time systems; stock markets; temporal logic; discrete-event concurrent systems; inference rules; online system; stock trading system; temporal Petri nets; temporal logic; Computer science; Formal specifications; Logic; Manufacturing systems; Petri nets; Power engineering and energy; Power system modeling; Stock markets; Timing; Turing machines;
Conference_Titel :
Computer Networks and Mobile Computing, 2001. Proceedings. 2001 International Conference on
Conference_Location :
Los Alamitos, CA
Print_ISBN :
0-7695-1381-6
DOI :
10.1109/ICCNMC.2001.962596
