The modeling, formal description and correctness verification of online static and dynamic stock trading systems, based on Shanghai Stock Exchange, are shown by using temporal Petri nets in order to make online stock trading systems more effective and rational. In the temporal Petri net models of the given static and dynamic systems, two types of tokens, namely data tokens representing trading data and control tokens used for keeping trading rules, are introduced. And the temporal constraint formulae are clearly and compactly represented by means of functional requirements of stock trading systems.The consistency between the functional requirements specifications of the online static and dynamic stock trading systems and the dynamic behavior of the temporal Petri net models is formally proved by means of the temporal logic operators to express temporal assertions.Also,certain promary reoperties of the temporal Petri new models are described and analyzed,such as liveness,fairness and safeness properties.It is further confirmed that temporal Petri nets are a promising descrbing and analyzing tool of discrete-event dynamic concurrent systems,and can describe explicitly certain time-related fundamental properties of concurrent systrms,such as eventuality and fairness.Finally the further study subjects are found.