Verifying functions in online stock trading systems

Temporal colored Petri nets, an extension of temporal Petri nets, are introduced in this paper. It can distinguish the personality of individuals (tokens), describe clearly the causal and temporal relationships between events in concurrent systems, and represent elegantly certain fundamental properties of concurrent systems, such as eventuality and fairness. The use of this method is illustrated with an example of modeling and formal verification of an online stock trading system. The functional correctness of the modeled system is formally verified based on the temporal colored Petri net model and temporal assertions. Also, some main properties of the system are analyzed. It has been demonstrated sufficiently that temporal colored Petri nets can verify efficiently some time-related properties of concurrent systems, and provide both the power of dynamic representation graphically and the function of logical inference formally. Finally, future work is described. This work is supported by the National Natural Science Foundation of China (Grant No.60125205), the National Grand Fundamental Research 973 Program of China (Grant Nos.2001AA413020, 2002AA4Z3430), the Open Project of Laboratory of Computer Science, Institute of Software, the Chinese Academy of Sciences (Grant Nos.SYSKF0205, SYSKF0309), Excellent Ph.D. Paper Author Foundation of China (Grant No.199934).