**ABSTRACT**

A dynamic stock trading system with a distributed shared memory is analyzed formally based on its temporal Petri net model. The functional correctness of the system is formally verified and some important properties of the system are investigated, such as liveness, fairness, safeness and temporal properties. Finally, conclusions are found.

PDF Abstract XML References Citation

####
**How to cite this article**

*Information Technology Journal, 7: 466-473.*

**DOI:**10.3923/itj.2008.466.473

**URL:**https://scialert.net/abstract/?doi=itj.2008.466.473

**INTRODUCTION**

Petri nets (PN) (Murata, 1989; Du *et al*., 2006) are a promising graphical and **mathematical modeling** tool for concurrent systems. However, PNs cannot describe explicitly some fundamental properties of the modeled systems, such as eventuality and fairness. In timed Petri nets (Berthomieu and Diaz, 1991; Du *et al*., 2007), moreover, the explicit introduction of time into them leads to very complicated formulae that tend to obscure the ideas about underlying causal and temporal relationships between events. Also, associating execution times or delays with transitions and places individually is inadequate for some of the fundamental properties. For this purpose, temporal Petri nets (TPN) are represented (Suzuki and Lu, 1989; Zurawski, 1997). TPNs can describe elegantly timing constraints, the dynamical behavior of a modeled system and causality between events on the basis of the formulae with temporal operators. The requirement specifications of a static stock trading system are represented based on the corresponding temporal logic formulae in Du *et al*. (2008) and the correctness of the system is verified based on its TPN model. While a dynamic stock trading system (DSTS) is modeled and specified by Zheng and Du (2005). In fact, the analysis of DSTSs is more difficult and complex than that of static stock trading systems. In this study, therefore, the dynamical behavior of a DSTS and the causality between events are analyzed based on its TPN model and the fundamental properties of the system are verified formally, such as liveness, fairness and safeness properties. This research is investigated based on Du *et al*. (2008) and Zheng and Du (2005). It is further demonstrated that TPNs own a stronger modeling and analysis power than PNs by the formal analysis and correctness verification of a DSTS and the performance of DSTSs can be improved and enhanced effectively.

As the suppositions in Zheng and Du (2005), a dynamical stock trading system is in a multiprocessor or multicomputer system with shared-variable DSM (Distributed Shared Memory). In general, the matches of deal data from all kinds of stocks are made in a multiprocessor or multicomputer system with a shared memory on a stock exchange. Each kind of stocks is dynamically assigned to a processor or a computer, on which matches of the deal data of this kind of stocks will be made. In a static case, the deal data of dozens or hundreds kinds of stocks will be fixedly processed on some processor or computer. In a dynamic case, however, the stock trading system uses a dynamic binding way to match up stocks and processors and the number of kinds of the stocks processed on some processor or computer is flexible. One of the primary functions of a DSTS is that processors make the matches of deal data by means of deal rules, such as First Price and First Time. Stock-brokers will send the deal data of stockholders to a stock exchange once verifying their validity. Their arriving time will be recorded by a prepositional computer on the stock exchange, then they be transferred to the multiprocessor system. The deal data are processed here and the trading results are sent to corresponding stock-brokers.

**TPN MODEL OF A DYNAMIC STOCK ****TRADING SYSTEM**

Some basic terminologies of PNs and TPNs are simply overviewed first in this section.

A PN is a 5-tuple, PN = (P, T; F, W, M_{0}), where P is a finite set of places; T is a finite set of transitions; F is a set of arcs; W: F → {1, 2, …} is a weight function and W is called an variable weight function if W(p, t) or W(t, p) is an variable; M_{0} is the initial marking. tεT is said to be firable at M iff ^{C}t: M(p) =W(p, t), where ^{•}t represents a set of the input places of t and (p, t) εF. Firing t at M will yield a new marking M', i.e., M[t>M', where

A TPN is a pair TPN=(PN, f), where f is a formula having the following syntax:

• | Propositions: p, t_{fir} and t are atomic propositions, where pεP, tεT |

• | Atomic propositions are formulae |

• | If f and g are formulae, so are –5 f, f +g, f•g, f ⇒g, οf, ◊f,□f |

The atomic propositions p, t_{fir} and t mean that there is at least one token in p, t is firable and t fires at the current marking, respectively. Symbols ¬, +, ≥ and ⇒ represent the Boolean connectives, NOT, OR, AND and IMPLICATION. Formula of means that f becomes true at the next marking reached. ∼f means that f becomes true at every marking reached from the current marking. ◊f means that f becomes eventually true at some marking reached from the current marking.

For any set S, S* represents the set of all finite sequences of elements of S, including the empty sequence λ. |α| represents the length of αε S*. αβ denotes the concatenation of α and β. For i: 0≤ i ≤*α|, let β_{i} and γ_{i} be the sequences such that |β_{i}| = i and α = β_{i} γ_{i}, β_{i} is the prefix of α with length i and γ_{i} is the postfix of α excluding β_{i}. Let M_{i} be a marking reached from M by firing β_{i}. Let f be a formula, <M, α>|- f means that f is satisfied by the pair of M and α, where |- represents a valid formula. Typical TPN formulae are defined as follows.

(a) | <M, α>|- p iff M(p)>0 |

(b) | <M, α>|- t_{fir} iff t is firable at M |

(c) | <M, α>|- t iff α ≠λ and t =β_{1}, i.e., t fires |

Fig. 1: | A subnet model of a prepositional computer processing system |

(d) | <M, α>|- ¬f iff not <M, α>|- f |

(e) | <M, α>|- f≥g iff <M, α>|- f and <M, α>|- g |

(f) | <M, α>|- f + g iff <M, α>|- f or <M, α>|- g |

(g) | <M, α>|- f ⇒g iff <M, α>|- f implies <M, α>|- g |

(h) | <M, α>|- Οf iff α ≠λ and <M_{1}, γ_{1} >|- f |

(i) | <M, α>|- ∼f iff <M_{i}, γ_{i} >|- f for every 0≤ i ≤|α | |

(j) | <M, α>|- ◊f iff <M_{i}, γ_{i} >|- f for some 0≤ i ≤|α | |

(k) | <M, α>|- f until g iff (<M_{i}, γ_{i} >|- f for every 0≤ i ≤|α|) or (<M_{i}, γ_{i} >|- g for some 0≤ i ≤|α| and <M_{j}, γ_{j} >|- f, for every 0≤ j ≤ i) |

The following properties can be easily proved by the above definitions.

PR_{1}: | <M, α>|- f +Οf implies <M, α>|- ◊f |

PR_{2:} | <M, α>|- ∼(f_{1}⇒f_{2})· ∼(f_{2}⇒f_{3}) implies <M, α>|- ∼ (f_{1}⇒ f_{3}) |

PR_{3}: | <M, α>|- ◊(◊f) implies <M, α>|- ◊f |

PR_{4} [5]: | <M, α>|- ∼ (t_{fir}⇒t) |

PR_{4} means that if t is firable for any possible firing sequence α at M, then t fires eventually.

In this study, only the processing processes of deal data on a prepositional computer and in multiple-processor system (Fig. 1) are modeled and analyzed using TPNs on a stock exchange. Therefore, the PN model (notation N_{D}) of a DSTS consists of a subnet of the prepositional computer processing system, a subnet of every processor pre-processing system and a subnet of every processor making match system. The subnets are shown in Fig.1-3, respectively.

Deal data of stockholders are usually divided into four classes: buying deal data, selling deal data, withdrawing buying and selling deal data. In Fig. 1, places SK-BK_{1}, SK-BK_{2},…, SK-BK_{m} contain the deal data from m stock-brokers, respectively; places p_{1}, p_{2},…and p_{n} contain the deal data of n kinds of stocks processed on the stock exchange, respectively. If there is one token in place pv_{i} (1≤i≤m), it means that the deal data in SK-BK_{i} have the privilege processed on the prepositional computer. The deal data in p_{0} will be classified based on the types of stocks, then sent to corresponding places p_{i} (1≤i≤n) by firing t_{Si}. A real arc means that it has a variable weight N. The doted arcs have an invariant weight 1 and denote the flow direction of the privilege. If transitions t_{pvi} and t_{SBi} (1≤i≤m) become firable, they must satisfy the following temporal formulas (ST_{1}) and (ST_{2}), respectively besides the firing conditions of the subnet in Fig. 1. For 1≤i≤m:

(ST_{1}): | ∼((t_{pvi})_{fir}⇒5SK_BK_{i}) |

(ST_{2}): | ∼((t_{SBi})_{fir}⇒5p_{0}) |

The formulas can be interpreted as in Zheng and Du (2005). When the deal data in SK-BK_{i} have gotten the privilege, if there is at least one token in it, then they do not deliver the privilege until t_{SBi} fires. But if it is empty here, the privilege must be transferred to the data in SK-BK_{i+1} by firing t_{pvi}. We obtain (ST_{1}). (ST_{2}) means that once the deal data with the privilege start to be processed on the prepositional computer, the other deal data do not be received until they are sent to the multiprocessor system.

In Fig. 2, if there is one token in the place pv_{ji} (1≤i≤n), it means that the deal data in p_{i} have the privilege. If there is one token in pro_{i}, it denotes that the deal data in p_{i} are being processed on some processor. When there is one token in p_{ji_2}, it means that the matches of the deal data in p_{i} are being made on the processor(j). p_{i_4} and p_{i_8} contain respectively the residual buying and selling deal data belonging to the kind of stock in p_{i}, after the matches of the deal data are made on some processor.

Assume that there are k processors in the multiple- processor system. Figure 2 shows the pre-processing process on every processor. That is, all processors have the same pre-processing way and the process of the matches made on every processor is also same. Every processor can process the deal data from all kinds of stocks. But the matches of the deal data of some kind of stocks can be made only on one processor at any moment. Therefore, places p_{i}, pro_{i}, p_{i_4} and p_{i_8} (1≤i≤n) are shared by all processors. Double-direction doted arcs connecting a transition t and a place p denote that p is not only an input place but also an output place of t and the number of tokens in p does not change after t fires.

Based on the previous discussion and deal rules, some transitions in Fig. 2 become firable only when they satisfy the following temporal formulas besides the firing conditions in this subnet. For 1≤i≤n, 1≤j≤k:

Fig. 2: | A subnet model of the processor(j) (1≤j≤k) pre-processing system |

(St_{3}): | ∼((t_{ji_1})_{fir}⇒5pro_{i}) |

(St_{4}): | ∼((t_{ji_2})_{fir} ⇒5p_{i}) |

(St_{5}): | ∼((t_{ji_4})_{fir} ⇒5p_{i_4} ≥¬p_{i_8}) |

(St_{6}): | ∼((t_{ji_9})_{fir} ⇒5pm_{j_4} ≥¬pm_{j_8}) |

These formulas can be interpreted as follows. (ST_{3}) means that if the matches of the deal data in p_{i} are being made on other processors, then they will not be processed on the processor (j) here. The interpretation of (ST_{4}) is similar to (ST_{1}). Since places p_{i_4} and p_{i_8} may contain respectively the residual buying and selling deal data after last one match of the deal data in p_{i} is made on some processor, the residual deal data must return to the processor (j) making system by firing t_{ji_5} and t_{ji_6} before the processor(j) makes the matches of the deal data in p_{ji_1}. We obtain (ST_{5}). (ST_{6}) can be interpreted similarly.

In Fig. 3, places TR and WD contain trading results and withdrawing deal data respectively, but they do not belong to the processor (j) trading system. They are two places in the processing system of stock-brokers. Places pm_{j_4} and pm_{j_8} deposit the buying and selling deal data, pm_{j_2} and pm_{j_11}, the withdrawing buying and selling deal data, respectively. By deal rules, if transitions t_{j_7}, t_{j_19}, t_{j_20} and t_{j_25} are firable, they must satisfy still the following temporal formulas (ST_{7})-(ST_{10}) respectively besides the firing conditions of the subnet in Fig. 3.

(ST_{7}): | ∼((t_{j_7})_{fir} ⇒5pm_{j_1} ≥ ¬pm_{j_24 }≥ ¬pm_{j_25}) |

(ST_{8}): | ∼((t_{j_19})_{fir} ⇒5pm_{j_1} ≥ ¬pm_{j_4 }≥ ¬pm_{j_25}) |

(ST_{9}): | ∼((t_{j_20})_{fir} ⇒5pm_{j_1} ≥ ¬pm_{j_24 }≥ ¬pm_{j_8}) |

(ST_{10}): | ∼((t_{j_25})_{fir} ⇒5pm_{j_7}) |

Formulas (ST_{7})-(ST_{10}) can be explained as follows. The datum with the highest buying price and the earliest arriving time in pm_{j_4} is transferred from pm_{j_4} to pm_{j_5} by firing t_{j_7}, the one with the lowest selling price and the earliest arriving time in pm_{j_8}, from pm_{j_8} to pm_{j_9} by firing t_{j_12}.

Fig. 3: | A subnet model of the processor (j) making match system |

If there is the withdrawing deal data in pm_{j_1}, they must be first withdrawn before t_{j_7} fires. We obtain (ST_{7}). If there is a token in pm_{j_19}, it means that processor(j) has made all matches of the deal data from p_{i} and prepare to process the other deal data having the privilege. A firing of t_{j_19} denotes that there is no buying deal datum in pm_{j_4} after at least one match of deal data is made or withdrawing deal data are removed, or there are only selling deal data in pm_{j_1} and they are transmitted to pm_{j_8}. Therefore, t_{j_19} can fire only when there is no token in pm_{j_1}, pm_{j_4} and pm_{j_25}. We obtain (ST_{8}). (ST_{9}) can be interpreted similarly. The deal datum with the highest buying price in pm_{j_5} is compared with the one with the lowest selling price in pm_{j_9} by firing t_{j_21}. If the price of the former is higher than that of the latter, t_{j_23} becomes firable, otherwise t_{j_22} becomes firable. A firing of t_{j_23} assures that this transaction has been clinched. By firing t_{j_9}, the trading results are sent to pm_{j_7}, a control token, to pm_{j_23}. The trading results in pm_{j_7} contain the data of matches made, the residual buying and selling deal data. Since a firing of t_{j_25} may cause a match made again, it becomes firable only when the data of matches made has been sent to place TR, the residual buying and selling deal data, to pm_{j_4} and pm_{j_8}, respectively. We obtain (ST_{10}).

Therefore, the TPN model of the system is a pair TND = (N_{D}, F_{D}), where N_{D} is a PN consisting of three subnets shown in Fig.1-3. And F_{D} is a set of formulas (ST_{1})-(ST_{10}).

**PROPERTIES ANALYSIS OF TPN MODEL TND**

Since a prepositional computer processes rotationally the deal data from all stock-brokers and they may concurrently send deal data to the corresponding places during deal, we suppose that the initial marking M_{0} of N_{D} contains the tokens in SK-BK_{i} (1≤i≤m) besides the control tokens shown in Fig. 1-2.

**Lemma 1: **(At any moment, the deal data of only one stock-broker have the privilege on the prepositional computer.) Let M be a marking reachable of TND from M_{0}, then for any firing sequence α from M, we have

Lemma 1 can be easily obtained by using the structure of the subnet in Fig.1. It presents a safeness property. Note that Lemma 1 is equivalent to the following conclusion.

<M, α>|– ∼ pv _{i}⇒ ¬pv_{r} |

where any α, i and r such that i≠r.

**Lemma 2: **(The fairness property for stock-brokers in a prepositional computer processing system.) Let M be a marking reachable of TND from M_{0}, then for any firing sequence α from M and any i, we have

<M, α>|–∼SK-BK _{i}⇒~t_{SBi} |

Lemma 2 can be proved by means of Lemma 1 and the structure of the subnet in Fig. 1. Lemma 2 means if there is at least one token in SK-BK_{i} at infinitely many markings, then t_{SBi} must fire infinitely often. On other words, if a stock-broker sends infinitely deal data to the prepositional computer, then they are often processed infinitely. A similar conclusion for all kinds of stocks is given as follows. It can be obtained by the structure of the subnet in Fig. 2.

**Lemma 3: **(The fairness property for stocks in a processor pre-processing system.) Let M be a marking reached of TND from M_{0}, then for any firing sequence α from M and any i, we have

<M, α>|–∼p _{i} ⇒~ pro_{i} |

Lemma 3 means that, if deal data of some kind of stock are infinitely sent on the prepositional computer to the multiprocessor system, the matches of them are infinitely made on the processors.

By the previous suppositions and the subnet in Fig. 2, places p_{i} and pro_{i} are shared on all processors. Thus, pro_{i} plays a mutual exclusion role in making the matches of the deal data in p_{i} on all processors.

**Lemma 4: **(The safeness (mutual exclusion) property for all kinds of stocks in processor pre-processing systems.) Let M be a marking reachable of TND from M_{0}. For any firing sequence α from M and any i and j, we have

**Proof: ** By the structure of the subnet in Fig. 2 and formula (a), pv_{ji} means that the processor (j) is at leisure at M; pro_{i} means that the former arriving deal data in p_{i} are being processed by some processor (r) (r≠ j). We obtain

<M, α>|–∼(p _{i} ≥pro_{i}≥ pv_{ji} ⇒ (t_{ji_3})_{fir}) | (1) |

(1) and PR_{4}, yield

<M, α>|–∼((t _{ji_3})_{fir} ⇒~t_{ji_3}) | (2) |

(1), (2), PR_{1} and PR_{2}, give

<M, α>|–∼ (p _{i}≥pro_{i}≥pv_{ji} ⇒~ t_{ji_3}) |

Lemma 4 shows that when the deal data in p_{i} are being processed on the processor(r), even if there are new arriving data in p_{i} and a processor (j) (j≠r) is at leisure, it does not make the matches of the deal data in p_{i} again. From Lemmas 3-4 and the structure of the subnet in Fig. 2, we can obtain the following conclusion.

**Lemma 5: **(At any moment, if the deal data from at least k kinds of stocks have arrived in processor pre-processing systems, then all processors will be eventually be busy at work.) Let M be a marking reached of TND from M_{0}, then for any firing sequence α and any i_{1}, i_{2},…, i_{r}ε{1, 2, …, n}, ∋j_{1}, j_{2}, … , j_{k}ε{i_{1}, i_{2},…, i_{r} }, where r = k, i_{u}≠i_{v} and j_{u}≠j_{v} when u≠v, we have

<M, α>|–∼ (p _{i1}≥p_{i2}≥ …$p_{ir}⇒(pro_{j1}≥pro_{j2}≥Y$pro_{jk})) |

Lemma 5 denote that if there are deal data waiting to be processed and the corresponding place pro_{i} contain non token in the multiprocessor system, then the matches of them will be eventually made on some processor.

**CORRECTNESS OF THE DYNAMIC STOCK TRADING SYSTEM**

Here, the major functional correctness of the DSTS modeled by TND will be verified. The following conclusions are deduced by means of the structures of the subnets in Fig. 1-3, temporal formulas (ST_{1})-(ST_{10}), TPN formulas (a)-(k) and TPN properties PR_{1}-PR_{4}. The requirements specification of the DSTS is described by the corresponding temporal logic formulas.

By the structure of the subnet in Fig. 3, (ST_{7}) and TPN formulas (k), the following lemma can be easily proved. Note the (t_{j_7})_{fir} means that places pm_{j_1}, pm_{j_24} and pm_{j_25} must be empty. And from deal rules, if there are withdrawing buying or selling deal data in pm_{j_1}, then there must be the corresponding buying or selling deal data in pm_{j_4} or pm_{j_8}, respectively. But if there are withdrawing (buying or selling) deal data in pm_{j_1} at M, then at least one place of them is not empty before t_{j_3} or t_{j_18} fires.

**Lemma 6: ** (If withdrawing deal data arrive on a processor, then they are first withdrawn before the processor begins to make a match.) Let M be a marking reachable of TND from M_{0}, then for any firing sequence α from M, we have

<M, α> |–∼((t _{j_1})_{fir}+(t_{j_16})_{fir} ⇒~ (¬(t_{j_7})_{fir} until (t_{j_3}+ t_{j_18}))) |

Lemma 6 illustrates that withdrawing buying or selling deal data have higher priority processed than buying or selling deal data in processor making match systems. This agrees with the deal rules of stocks.

**Lemma 7: **(If the deal data of some kind of stock arrive in a processor making match system, then the processor will eventually finish making all matches of them.) Let M be a making reachable of TND from M_{0}. For any firing sequence α from M, we have

<M, α> |–∼(pm _{j_1}⇒ ◊ pm_{j_19}) |

**Proof: ** Given that the deal data are being processed on the processor (j). By the structure of the subnet in Fig. 3, we obtain

<M, α> |–∼(pm _{j_1}⇒(t_{j_1})_{fir} +(t_{j_16})_{fir} +(t_{j_6})_{fir} +(t_{j_11})_{fir}) | (3) |

(3) and formula (f), yield

<M, α> |–∼(pm _{j_1}⇒(t_{j_6})_{fir} +(t_{j_11})_{fir}) | (4) |

or <M, α>|–∼(pm _{j_1}⇒(t_{j_1})_{fir} +(t_{j_16})_{fir}) | (5) |

Here, the proof of the states, which only (4) is valid is valid, will be shown as follows to save space.

Since a firing of t_{j_7} requires that pm_{j_1} is empty, if t_{j_6} and t_{j_11} are firable, then they must fire successively. Thus, from (4), formula (f) and PR_{4}, we have

<M, α> |–∼(t _{j_6} +t_{j_11} ⇒((pm_{j_4}+ pm_{j_8}) ≥pm_{j_15} ≥¬pm_{j_1})) | (6) |

Because pm_{j_24} and pm_{j_25} are empty, if one of pm_{j_4} and pm_{j_8} is empty, then the lemma is proved by firing t_{j_19} or t_{j_20} from (ST_{8}) or (ST_{9}). Therefore, we suppose that pm_{j_4} and pm_{j_8} are nonempty. By (6) and PR_{1} we have

<M, α> |–∼(t _{j_12 }⇒ (pm_{j_5 }≥ pm_{j_9})) | (7) |

<M, α> |–∼(pm _{j_5 }≥ pm_{j_9 }⇒(t_{j_21})_{fir}) | (8) |

<M, α> |–∼(t _{j_21 }⇒ (pm_{j_5}≥ pm_{j_9} ≥ pm_{j_18})) | (9) |

Based on trading rules, here there is the deal datum with the highest buying price in pm_{j_5}, the deal datum with the lowest selling price in pm_{j_9}. If the price of the former is less than that of the latter, then t_{j_22} is firable, otherwise t_{j_23} is firable. Therefore, two cases can be respectively discussed as follows.

CASE 1: <M, α> |–∼(pm _{j_5}≥ pm_{j_9} ≥ pm_{j_18 }⇒(t_{j_22})_{fir}) | (10) |

By (10), PR_{4} and formulas (e), (g), (i), we have

<M, α> |– ∼(pm _{j_1}⇒ pm_{j_19}) |

CASE 2: <M, α> |–∼ (pm _{j_5 }≥ pm_{j_9} ≥ pm_{j_18 }⇒(t_{j_23})_{fir}) | (11) |

From (11), PR_{4} and the structure of the subnet in Fig. 3, we obtain

<M, α> |–∼(t _{j_9 }⇒ (pm_{j_7 }≥ pm_{j_23})) | (12) |

Here, there must be a deal result in pm_{j_7}, but it may also contain residual parts of the buying and selling deal data. We have

<M, α> |–∼(pm | (13) |

From trading rules and (13), t_{j_10} must be firable. If there is a residual buying (selling) deal datum, then t_{j_5}(t_{j_15}) is also firable. Therefore, whichever in the four cases exists, their deductive processes are similar. Now we only discuss the first case, i.e.,

<M, α> |–∼(pm _{j_7 }≥ pm_{j_23 }⇒(t_{j_10})_{fir}) | (14) |

From (ST_{10}) and PR_{4}, we have

<M, α> |–∼(t _{j_25 }⇒pm_{j_15}) | (15) |

From (15), if t_{j_7} is firable now, the inferring process of (7)-(15) is repeatedly done until the conclusion of this lemma is obtained. If t_{j_7} is not firable, a valid formula is given as followings by (ST_{8}) and (ST_{9}):

<M, α> |–∼(pm _{j_15}⇒(t_{j_19})_{fir}+(t_{j_20})_{fir}) | (16) |

(16), formulas (i), (g), (f) and PR_{4}, yield

<M, α> |–∼(t _{j_19}+t_{j_20} ⇒pm_{j_19}) | (17) |

By 4, 6-9, 11-17, formula (f) and PR_{1}, PR_{2}, we obtain

<M, α> |–∼(pm _{j_1}⇒ pm_{j_19}) |

Lemma 7 shows the liveness (no deadlock, no lockout) property in every processor making match system. The following theorem presents the global liveness property in processor processing systems.

**Theorem 1: **(If a processor begins to process the deal data of some kind of stock, then it will eventually finish making all matches of them and deliver the privilege to another kind of stock.) Let M be a marking reachable of TND from M_{0}, then for any firing sequence α from M and any i, 1≤j≤k, we have

<M, α> |–∼(p _{i} ≥pv_{ji }≥ ¬pro_{i} ⇒ ◊ pv_{j(i+1)}) |

**Proof: **By the structure of the subnet in Fig. 2, PR4 and (ST_{3}), we have

<M, α> |–∼(t _{ji_1 }⇒ (pro_{i} ≥ p_{ji_1})) | (18) |

Here, if one of p_{i_4} and p_{i_8} is nonempty, then all residual deal data in p_{i_4} or p_{i_8} can be transferred to pm_{j_4} or pm_{j_8} by firing t_{ji_5} or t_{ji_6}, respectively. Therefore, we suppose that they are empty. From (18), PR4 and (ST_{5}), we have

<M, α> |–∼(t _{ji_4 }⇒ (pro_{i} ≥ pm_{j_1} ≥ p_{ji_2})) | (19) |

By Lemma 7, (19) and formula (e), we have

<M, α> |–∼(pro _{i} ≥ pm_{j_1} ≥ p_{ji_2 }⇒ (pro_{i} ≥ pm_{j_19} ≥ p_{ji_2})) | (20) |

Similarly, we suppose that pm_{j_4} and pm_{j_8} are empty. Otherwise, they will be empty after firing t_{ji_7} or t_{ji_8}. Thus, from (20), PR4 and (ST_{6}), we have

<M, α> |–∼(t _{ji_9 }⇒ pv_{j(i+1)}) | (21) |

From 18-21 and PR_{1}, PR_{2}, we obtain

<M, α> |–∼(p _{i} ≥pv_{ji }≥ ¬pro_{i} ⇒ pv_{j(i+1)}) |

By means of the structures of the subnets in Fig. 1-3, Lemmas 2-7, Theorem 1 and their proofs, Theorems 2 and 3 can be given below. Their proofs are omitted to save space.

**Theorem 2: **TND is live, safe, fair and bounded.

**Theorem 3: **The dynamic behavior of TND is consistent with the functional requirements of DSTSs.

**CONCLUSIONS**

It is demonstrated further that TPNs can not only enhance the modeling and analysis power of PNs, but also compensate the shortcoming that PNs do not represent timing constraints, such as eventuality. In doing so, a DSTS with shared-variable DSM is adopted. It has been formally proved that the functional requirements of the system can be satisfied by the dynamic behavior of TPN model TND. Also, the correctness of the system is analyzed and verified based on its TPN model. A main defect of TPNs is the lack of variables for describing the values and types of data items. Therefore, the price and types of deal data could not be explicitly described in the TPN model. However, if these properties are required, we may use colored TPNs (Du and Jiang, 2004) to model and verify the systems.

In the subnet of processor pre-processing systems, every processor processes dynamically the deal data of all kinds of stocks. Processors may spend much more time to seek the deal data waiting to be processed. To cope with this problem, n kinds of stocks divide into k sets and every set is fixedly assigned to one processor. When some processor is at leisure, it will seek the deal data belonging to the set on the other processors. In this case, the analysis methods proposed in this paper are still valid. The performance analysis and evaluation of DSTSs will be investigated in future using stochastic PNs.

**ACKNOWLEDGMENTS **

This research was supported in part by the National Natural Science Foundation of China under Grants 60773034, 60534060 and 60473094; the Taishan Scholar Construction Project of Shandong Province, China; the National Basic Research Program of China (973 Program) under Grants 2007CB316502 and 2004CB318001-03; the Open Project of the State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences under Grant SYSKF0804 and the Research foundation of East China University of Science and Technology.

####
**REFERENCES**

- Berthomieu, B. and M. Diaz, 1991. Modeling and verification of time dependent systems using time petri nets. IEEE Trans. Software Eng., 17: 259-273.

CrossRefDirect Link - Du, Y.Y. and C.J. Jiang, 2004. Verifying functions in online stock trading systems. J. Comput. Sci. Technol., 19: 203-212.

CrossRefDirect Link - Du, Y., C. Jiang and Y. Guo, 2006. Towards a formal model for grid architecture via petri nets. Inform. Technol. J., 5: 833-841.

CrossRefDirect Link - Du, Y.Y., C.J. Jiang and M.C. Zhou, 2007. Modeling and analysis of real-time cooperative systems using petri nets. IEEE Trans. Syst. Man Cybern. Part A: Part A: Syst. Hum., 37: 643-654.

CrossRefDirect Link - Du, Y.Y., C.J. Jiang and M.C. Zhou, 2008. A petri-net-based correctness analysis of internet stock trading systems. IEEE Trans. Syst. Man Cybern. Part C: Appl. Rev., 38: 93-99.

CrossRefDirect Link - Murata, T., 1989. Petri nets: Properties, analysis and applications. Proc. IEEE., 77: 541-580.

CrossRefDirect Link - Zurawski, R., 1997. Verifying correctness of interfaces of design models of manufacturing systems using functional abstractions. IEEE Trans. Ind. Elect., 44: 307-320.

CrossRefDirect Link