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

fYear

2001

fDate

2001

Firstpage

197

Lastpage

202

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Computer Networks and Mobile Computing, 2001. Proceedings. 2001 International Conference on

Conference_Location

Los Alamitos, CA

Print_ISBN

0-7695-1381-6

Type

conf

DOI

10.1109/ICCNMC.2001.962596

Filename

962596