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.
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, M0), 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; M0 is the initial marking. tεT is said to be firable at M iff Ct: 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, tfir 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, tfir 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 Mi 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, α>|- tfir 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 <M1, γ1 >|- f |
| (i) | <M, α>|- ∼f iff <Mi, γi >|- f for every 0≤ i ≤|α | |
| (j) | <M, α>|- ◊f iff <Mi, γi >|- f for some 0≤ i ≤|α | |
| (k) | <M, α>|- f until g iff (<Mi, γi >|- f for every 0≤ i ≤|α|) or (<Mi, γi >|- g for some 0≤ i ≤|α| and <Mj, γj >|- f, for every 0≤ j ≤ i) |
The following properties can be easily proved by the above definitions.
| PR1: | <M, α>|- f +Οf implies <M, α>|- ◊f |
| PR2: | <M, α>|- ∼(f1⇒f2)· ∼(f2⇒f3) implies <M, α>|- ∼ (f1⇒ f3) |
| PR3: | <M, α>|- ◊(◊f) implies <M, α>|- ◊f |
| PR4 [5]: | <M, α>|- ∼ (tfir⇒t) |
PR4 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 ND) 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-BK1, SK-BK2,…, SK-BKm contain the deal data from m stock-brokers, respectively; places p1, p2,…and pn contain the deal data of n kinds of stocks processed on the stock exchange, respectively. If there is one token in place pvi (1≤i≤m), it means that the deal data in SK-BKi have the privilege processed on the prepositional computer. The deal data in p0 will be classified based on the types of stocks, then sent to corresponding places pi (1≤i≤n) by firing tSi. 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 tpvi and tSBi (1≤i≤m) become firable, they must satisfy the following temporal formulas (ST1) and (ST2), respectively besides the firing conditions of the subnet in Fig. 1. For 1≤i≤m:
| (ST1): | ∼((tpvi)fir⇒5SK_BKi) |
| (ST2): | ∼((tSBi)fir⇒5p0) |
The formulas can be interpreted as in Zheng and Du (2005). When the deal data in SK-BKi have gotten the privilege, if there is at least one token in it, then they do not deliver the privilege until tSBi fires. But if it is empty here, the privilege must be transferred to the data in SK-BKi+1 by firing tpvi. We obtain (ST1). (ST2) 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 pvji (1≤i≤n), it means that the deal data in pi have the privilege. If there is one token in proi, it denotes that the deal data in pi are being processed on some processor. When there is one token in pji_2, it means that the matches of the deal data in pi are being made on the processor(j). pi_4 and pi_8 contain respectively the residual buying and selling deal data belonging to the kind of stock in pi, 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 pi, proi, pi_4 and pi_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 |
| (St3): | ∼((tji_1)fir⇒5proi) |
| (St4): | ∼((tji_2)fir ⇒5pi) |
| (St5): | ∼((tji_4)fir ⇒5pi_4 ≥¬pi_8) |
| (St6): | ∼((tji_9)fir ⇒5pmj_4 ≥¬pmj_8) |
These formulas can be interpreted as follows. (ST3) means that if the matches of the deal data in pi are being made on other processors, then they will not be processed on the processor (j) here. The interpretation of (ST4) is similar to (ST1). Since places pi_4 and pi_8 may contain respectively the residual buying and selling deal data after last one match of the deal data in pi is made on some processor, the residual deal data must return to the processor (j) making system by firing tji_5 and tji_6 before the processor(j) makes the matches of the deal data in pji_1. We obtain (ST5). (ST6) 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 pmj_4 and pmj_8 deposit the buying and selling deal data, pmj_2 and pmj_11, the withdrawing buying and selling deal data, respectively. By deal rules, if transitions tj_7, tj_19, tj_20 and tj_25 are firable, they must satisfy still the following temporal formulas (ST7)-(ST10) respectively besides the firing conditions of the subnet in Fig. 3.
| (ST7): | ∼((tj_7)fir ⇒5pmj_1 ≥ ¬pmj_24 ≥ ¬pmj_25) |
| (ST8): | ∼((tj_19)fir ⇒5pmj_1 ≥ ¬pmj_4 ≥ ¬pmj_25) |
| (ST9): | ∼((tj_20)fir ⇒5pmj_1 ≥ ¬pmj_24 ≥ ¬pmj_8) |
| (ST10): | ∼((tj_25)fir ⇒5pmj_7) |
Formulas (ST7)-(ST10) can be explained as follows. The datum with the highest buying price and the earliest arriving time in pmj_4 is transferred from pmj_4 to pmj_5 by firing tj_7, the one with the lowest selling price and the earliest arriving time in pmj_8, from pmj_8 to pmj_9 by firing tj_12.
| Fig. 3: | A subnet model of the processor (j) making match system |
If there is the withdrawing deal data in pmj_1, they must be first withdrawn before tj_7 fires. We obtain (ST7). If there is a token in pmj_19, it means that processor(j) has made all matches of the deal data from pi and prepare to process the other deal data having the privilege. A firing of tj_19 denotes that there is no buying deal datum in pmj_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 pmj_1 and they are transmitted to pmj_8. Therefore, tj_19 can fire only when there is no token in pmj_1, pmj_4 and pmj_25. We obtain (ST8). (ST9) can be interpreted similarly. The deal datum with the highest buying price in pmj_5 is compared with the one with the lowest selling price in pmj_9 by firing tj_21. If the price of the former is higher than that of the latter, tj_23 becomes firable, otherwise tj_22 becomes firable. A firing of tj_23 assures that this transaction has been clinched. By firing tj_9, the trading results are sent to pmj_7, a control token, to pmj_23. The trading results in pmj_7 contain the data of matches made, the residual buying and selling deal data. Since a firing of tj_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 pmj_4 and pmj_8, respectively. We obtain (ST10).
Therefore, the TPN model of the system is a pair TND = (ND, FD), where ND is a PN consisting of three subnets shown in Fig.1-3. And FD is a set of formulas (ST1)-(ST10).
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 M0 of ND contains the tokens in SK-BKi (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 M0, 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, α>|– ∼ pvi⇒
¬pvr |
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 M0, then for any firing sequence α from M and any i, we have
| <M, α>|–∼SK-BKi⇒~tSBi |
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-BKi at infinitely many markings, then tSBi 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 M0, then for any firing sequence α from M and any i, we have
| <M, α>|–∼pi
⇒~ proi |
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 pi and proi are shared on all processors. Thus, proi plays a mutual exclusion role in making the matches of the deal data in pi 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 M0. 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), pvji means that the processor (j) is at leisure at M; proi means that the former arriving deal data in pi are being processed by some processor (r) (r≠ j). We obtain
|
<M, α>|–∼(pi
≥proi≥ pvji ⇒ (tji_3)fir)
|
(1) |
(1) and PR4, yield
|
<M, α>|–∼((tji_3)fir
⇒~tji_3) |
(2) |
(1), (2), PR1 and PR2, give
| <M, α>|–∼
(pi≥proi≥pvji ⇒~ tji_3) |
Lemma 4 shows that when the deal data in pi are being processed on the processor(r), even if there are new arriving data in pi and a processor (j) (j≠r) is at leisure, it does not make the matches of the deal data in pi 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 M0, then for any firing sequence α and any i1, i2,…, irε{1, 2, …, n}, ∋j1, j2, … , jkε{i1, i2,…, ir }, where r = k, iu≠iv and ju≠jv when u≠v, we have
| <M, α>|–∼
(pi1≥pi2≥ …$pir⇒(proj1≥proj2≥Y$projk)) |
Lemma 5 denote that if there are deal data waiting to be processed and the corresponding place proi 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 (ST1)-(ST10), TPN formulas (a)-(k) and TPN properties PR1-PR4. The requirements specification of the DSTS is described by the corresponding temporal logic formulas.
By the structure of the subnet in Fig. 3, (ST7) and TPN formulas (k), the following lemma can be easily proved. Note the (tj_7)fir means that places pmj_1, pmj_24 and pmj_25 must be empty. And from deal rules, if there are withdrawing buying or selling deal data in pmj_1, then there must be the corresponding buying or selling deal data in pmj_4 or pmj_8, respectively. But if there are withdrawing (buying or selling) deal data in pmj_1 at M, then at least one place of them is not empty before tj_3 or tj_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 M0, then for any firing sequence α from M, we have
| <M, α> |–∼((tj_1)fir+(tj_16)fir
⇒~ (¬(tj_7)fir until (tj_3+
tj_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 M0. For any firing sequence α from M, we have
| <M, α> |–∼(pmj_1⇒
◊ pmj_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, α> |–∼(pmj_1⇒(tj_1)fir
+(tj_16)fir +(tj_6)fir
+(tj_11)fir) |
(3) |
(3) and formula (f), yield
| <M, α> |–∼(pmj_1⇒(tj_6)fir
+(tj_11)fir) |
(4) |
| or <M, α>|–∼(pmj_1⇒(tj_1)fir
+(tj_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 tj_7 requires that pmj_1 is empty, if tj_6 and tj_11 are firable, then they must fire successively. Thus, from (4), formula (f) and PR4, we have
| <M, α> |–∼(tj_6
+tj_11 ⇒((pmj_4+ pmj_8)
≥pmj_15 ≥¬pmj_1)) |
(6) |
Because pmj_24 and pmj_25 are empty, if one of pmj_4 and pmj_8 is empty, then the lemma is proved by firing tj_19 or tj_20 from (ST8) or (ST9). Therefore, we suppose that pmj_4 and pmj_8 are nonempty. By (6) and PR1 we have
| <M, α> |–∼(tj_12
⇒ (pmj_5 ≥ pmj_9)) |
(7) |
| <M, α> |–∼(pmj_5
≥ pmj_9 ⇒(tj_21)fir) |
(8) |
| <M, α> |–∼(tj_21
⇒ (pmj_5≥ pmj_9 ≥ pmj_18)) |
(9) |
Based on trading rules, here there is the deal datum with the highest buying price in pmj_5, the deal datum with the lowest selling price in pmj_9. If the price of the former is less than that of the latter, then tj_22 is firable, otherwise tj_23 is firable. Therefore, two cases can be respectively discussed as follows.
| CASE 1: <M, α>
|–∼(pmj_5≥ pmj_9 ≥ pmj_18
⇒(tj_22)fir) |
(10) |
By (10), PR4 and formulas (e), (g), (i), we have
|
<M, α> |– ∼(pmj_1⇒
pmj_19) |
| CASE 2: <M, α>
|–∼ (pmj_5 ≥ pmj_9 ≥ pmj_18
⇒(tj_23)fir) |
(11) |
From (11), PR4 and the structure of the subnet in Fig. 3, we obtain
| <M, α> |–∼(tj_9
⇒ (pmj_7 ≥ pmj_23)) |
(12) |
Here, there must be a deal result in pmj_7, but it may also contain residual parts of the buying and selling deal data. We have
|
<M, α> |–∼(pmj_7≥pmj_23⇒(tj_10)fir+(tj_10)fir≥(tj_5)fir |
(13) |
From trading rules and (13), tj_10 must be firable. If there is a residual buying (selling) deal datum, then tj_5(tj_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, α> |–∼(pmj_7
≥ pmj_23 ⇒(tj_10)fir)
|
(14) |
From (ST10) and PR4, we have
| <M, α> |–∼(tj_25
⇒pmj_15) |
(15) |
From (15), if tj_7 is firable now, the inferring process of (7)-(15) is repeatedly done until the conclusion of this lemma is obtained. If tj_7 is not firable, a valid formula is given as followings by (ST8) and (ST9):
| <M, α> |–∼(pmj_15⇒(tj_19)fir+(tj_20)fir) |
(16) |
(16), formulas (i), (g), (f) and PR4, yield
| <M, α> |–∼(tj_19+tj_20
⇒pmj_19) |
(17) |
By 4, 6-9, 11-17, formula (f) and PR1, PR2, we obtain
|
<M, α> |–∼(pmj_1⇒
pmj_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 M0, then for any firing sequence α from M and any i, 1≤j≤k, we have
| <M, α> |–∼(pi
≥pvji ≥ ¬proi ⇒ ◊ pvj(i+1))
|
Proof: By the structure of the subnet in Fig. 2, PR4 and (ST3), we have
| <M, α> |–∼(tji_1
⇒ (proi ≥ pji_1)) |
(18) |
Here, if one of pi_4 and pi_8 is nonempty, then all residual deal data in pi_4 or pi_8 can be transferred to pmj_4 or pmj_8 by firing tji_5 or tji_6, respectively. Therefore, we suppose that they are empty. From (18), PR4 and (ST5), we have
| <M, α> |–∼(tji_4
⇒ (proi ≥ pmj_1 ≥ pji_2)) |
(19) |
By Lemma 7, (19) and formula (e), we have
|
<M, α> |–∼(proi
≥ pmj_1 ≥ pji_2 ⇒ (proi
≥ pmj_19 ≥ pji_2)) |
(20) |
Similarly, we suppose that pmj_4 and pmj_8 are empty. Otherwise, they will be empty after firing tji_7 or tji_8. Thus, from (20), PR4 and (ST6), we have
| <M, α> |–∼(tji_9
⇒ pvj(i+1)) |
(21) |
From 18-21 and PR1, PR2, we obtain
|
<M, α> |–∼(pi
≥pvji ≥ ¬proi ⇒ pvj(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.