CN105183652B - Pushed net under time dynamic the conversion method of network - Google Patents

Abstract

The present invention discloses a kind of conversion method for network of being pushed net under time dynamic, for the Real-time and Concurrent recusive modeling for describing to create containing recurrence, dynamic thread.The global clock of description continuous time is introduced first in DPN, and real number clock with time correlation global variable and stack character " age " can be described, so as to be modeled to carrying out asynchronous communication based on shared drive, and with the Real-time and Concurrent system that dynamic thread creates.Secondly to the clock equivalent technique based on integer partitioning, a kind of optimisation technique based on clock key point, reduction clock section, so as to reduce the state space after conversion are provided.Because network of being pushed net under time dynamic is a kind of abstract model of Real-time and Concurrent recursive program, clock equivalence optimisation technique based on key point is network of being pushed net under dynamic the model conversion, so by confirming whether the execution that network model is pushed away under dynamic can run to error condition, so as to detect the mistake or leak in the i.e. corresponding concurrent recursive program of this model.

Description

Pushed net under time dynamic the conversion method of network

Technical field

The invention belongs to software security and reliability consideration field, it is related to the authentication of multi-thread concurrent recursive program Method, it is a kind of accessibility solution technique suitable for the multi-thread concurrent recursive program abstract model containing having time, and in particular to Pushed net under a kind of time dynamic the conversion method of network.

Background technology

With the development of multi-core technology, concurrent program has turned into the focus of present procedure design studies.Due to concurrently performing In the presence of uncertainty, so as to cause conventional test methodologies to be difficult the mistake and leak hidden in discovery procedure.Model testing is one The automatic Verification technology that kind passes through exhaustive search, it has also become ensure program safety and reliable important means, test can be used as A kind of supplement of method.Approachability analysis is the important core technology of model testing by analyzing whether a certain state is reachable.

In recent years, researcher is based on automaton model, real-time clock is introduced, for describing real time system modelling and its testing Card.Alur proposes Timed Automata (R.Alur, D.Dill, A theory of timed automata [J] within 1994 .Theoretical Computer Science, 126 (2), pp.183-235,1994.) it is to be introduced on the basis of automatic machine The clock of continuous time is described, and gives clock equivalent technique, so as to implementation model Check-Out Time automatic machine (J.Bengtsson, W.Yi, Timed automata:Semantics, algorithms and tools [C], 4th Advanced Course on Petri Nets, Eichstaat.Germany, pp.87-124,2004).In order to solve containing Recursive real time system modelling, Trivedi (A.Trivedi, D.Wojtczak, Recursive Timed Automata [C], ATVA 2010.LNCS, vol.6252, Springer, Heidelberg, pp.306-324.2010.) propose to push away under the time automatically Machine, and time pushdown automata is converted to by clock equivalent technique by pushdown automata, solve the reachable of minimum time cost Sex chromosome mosaicism.Li in 2013 (L G qiang, C X juan, O.Mizuhito, Nested Timed Automata [R], Research report (School of Information Science, Japan Advanced Institute of Science and Technology), IS-RR-2013-004, pp.1-20,2013) nested Timed Automata is proposed, utilize Nested thought solves the recurring problem in real-time system.But this class model can not be described with the real-time of dynamic thread establishment Concurrent system modeling.Bouajjani (A.Bouajjani, M.M.Olm, T.Touili.Regular symbolic analysis of dynamic networks of pushdown systems[C].Proceedings of the 16th International Conference on Concurrency Theory.LNCS 3653, San Francisco:Cisco Syst, 2005,473-487.) propose a kind of and give pushing system (B.Bollig, D.Kuske, R.Mennicke, The Complexity of model checking multi-stack systems [C], Proceedings of The201328th Annual ACM/IEEE Symposium on Logic in Computer Science, New Orleans, LA, USA, pp.163-72,2013) extended model --- network (DPN) of being pushed net under dynamic, solve concurrent system in The dynamic creation of new thread, the model are applied to the concurrent system modeling created containing recurrence and with dynamic thread.It is based on DPN, Lammich (P.Lammich, M.M.Olm, H.Seidl, Contextual Locking for Dynamic Pushdown Networks [C] .Static Analysis.Proceedings of 20th International Symposium, Seattle, WA, USA, pp.47-98,2013.) technology that context is locked is proposed, solve stationary problem between process recurrence, And reverse reachability analysis is carried out.Wenner (A.Wenner, Weighted dynamic pushdown networks [C], 19th European symposium on programming, Paphos, Cyprus, pp.590-609,2010.) in DPN Weights are introduced, for solving the accessibility of shortest path.

Because above-mentioned model can not describe the situation of interaction between the concurrent recursive system thread of real-time multithread, for real-time For multi-thread concurrent recursive program, this class method of Formal Verification will produce State-explosion problem, be brought to checking Extreme difficulties.

The content of the invention

The technical problems to be solved by the invention are to provide a kind of conversion method for network of being pushed net under time dynamic, and its time is moved Network of being pushed net under state is a kind of abstract model of Real-time and Concurrent recursive program, and the clock equivalence optimisation technique based on key point is the mould Type is converted to network of being pushed net under dynamic, so by confirming whether the execution that network model is pushed away under dynamic can run to error condition, So as to detect the mistake or leak in the i.e. corresponding concurrent recursive program of this model.

To solve the above problems, the present invention is achieved by the following technical solutions：

Push net the conversion method of network, comprise the following steps under time dynamic：

Described Real-time and Concurrent recursive program is converted to network of being pushed net under a time dynamic by step (1).

The abstract model of step (1.1) construction Real-time and Concurrent recursive program is network of being pushed net under time dynamic.

Network of being pushed net under the time dynamic constructed is a four-tuple T=(P, Γ, Δ, X), wherein：P is state set；Γ It is stack character set；Δ=Δ_nop∪Δ₌∪Δ_├∪Δ_push∪Δ_pop∪Δ_dcIt is migration rules set, wherein Δ_nopRepresent empty Operation migration, Δ₌Represent the migration of clock assignment, Δ_├Represent time passage migration, Δ_pushRepresent stacking migration, Δ_popRepresent Stack migrates, Δ_dcRepresent that dynamic thread creates migration；X represents clock collection, its value functionRepresent forIt is θ (x) in current value, it is also similar therewith with the global variable and stack character " age " value of time correlation.

Network situation is pushed away under institute's build time dynamicRepresent the shape of the model at a time State, wherein：Represent current global variable g and its " age " θ (g) two tuples<g,θ(g)>； p_i∈ P represent local state node,Represent the stack content ω that stack sequence is i_iWith its " age " θ (ω_i) two tuples<ω_i,θ (ω_i)>；Represent clock x and its value θ (x) two tuples<x,θ(x)>.

Network of being pushed net under the time dynamic constructed is described step (1.2) with operational semantics.

Pushed net under time dynamic model of the network as real-time multithread program, for describing multiple lower pushing systems while producing Migration, its transition relationship Δ=Δ_nop∪Δ₌∪Δ_├∪Δ_push∪Δ_pop∪Δ_dcProvided below according to different migration actions It performs implication；

1) Δ=Δ_nopWhen, op=nop,Represent that general layout interior element does not change；

2) Δ=Δ₌When, op=x ← I,c∈I；It is represented to clock x and specifies I scopes Interior arbitrary value v, other general layout interior elements do not change；

3) Δ=Δ_├When, op=Time ← c,Assuming thatSoAll clocks increase v in general layout are represented, when non-in general layout Clock content does not change；

4) Δ=Δ_pushWhen, op=push (a, I),V ∈ I,Variable a is pressed into by expression Stack top, and corresponding clock is set as x, its clock value is the arbitrary value in the range of I；

5) Δ=Δ_popWhen, op=pop (a, I),V ∈ I,Represent stack top internal clock value Ejected for the variable a of I scopes；

6) Δ=Δ_dcWhen, op=dc,Represent to create new thread stack content.

Push net network T=(P, Γ, Δ, X) under the time dynamic that step (2) is obtained step (1), passes through following conversion sides Method is converted to the network M=(P that pushed net under dynamic^M,Γ^M,Δ^M)；

Step (2.1) state P^MConversion：I.e. T state set is identical with M state set.

Step (2.2) stack character setConversion：If a ∈ { Γ, ├ }, thenAnd

Step (2.3) transition relationship Δ is to Δ^MTransformation rule.

Assuming that the TDPN currently containing n stack, for convenience, only describes the lower pushing system that sequence is i and performs pop down And Pop operations, other stack operations are similar therewith.If the stack level of the lower pushing system is l, and stack bottom numbering is 1, stack top numbering For l.The TDPN contains global variable g, clock variable x, stack content ω={ ω₁…ω_i…ω_n, wherein ω_iRepresent to push away under No. i The stack content of system, uses ω_il|ΓRepresent ω_iIt is projected in Γ stack top character.Each table Show its key point of " age " and value under clock equivalence.It is corresponding in M present clock equivalence domain so as to understand WhereinRepresentative domain R_lRecord stack top character, ├ tables Show domain R_lReference clock character, ├^·Representative domain R_lCorresponding time passage character.

TDPN general layoutsφ=(γ, op, γ ') ∈ Δs represent T general layout migration, corresponding M lattice Office's migration is represented byWherein p and p ' is identical with state in T, before representing general layout migration respectively State afterwards；R_l={ R_1l…R_il…R_nlRepresent stack top domain, wherein R_ilRepresent the stack top domain of No. i lower pushing system, R_lAnd R_l' respectively Represent the front and rear stack top domain of general layout migration；Action migration collection op ' correspond to T op, below mainly describe according to different op structures Make R_l′：

1) as op=nop, forExist in and if only if M State is only changed in T hollow operations, so general layout migration also only changes state, domain R in M_lKeep constant.

2) as op=(x ← I), forExist in and if only if M The transition relationship is represented to DPN domains R_lThe item that middle clock is x performsBehaviour Make, wherein θ (x) ' ∈ I, carry out structural domain R_l′.Specific implementation procedure is as follows：

● domain R_lPop, obtain R_lIn itemIt is θ (x) ' to reset θ (x), forms new item

● itemInstead of domain R_lIn itemObtain domain R_l', and stacking, it is transformed into new state p′。

3) as op=(Time ← v), forExist in and if only if M Transition relationship representative domain R_lIn except reference clock item (├, 0), remaining all when Clock value carrys out structural domain R plus time passage v_l ⁺.Specifically performing step is：

● domain R_lPop, except reference clock, all passed v plus the time, Expression corresponds to g, ω_il, x new general term,Respectively represent corresponding new record ,Represent reference clock entry；

● new item replaces original item, obtains domain R_l ⁺, and stacking, it is transformed into new state p '.

4) as op=push (a, I), forAnd if only if, and M is present The transition relationship represents, carries out stack-incoming operation to No. i lower pushing system, is by character A, is worth and isItem stacking domain R_il, carry out structural domain R_i(l+1).Detailed process is as follows：

● from R_ilObtain itemWith

●Respectively instead of Obtain domain R_i(l+1), and stacking, it is transformed into new state p '.

5) as op=pop (a, I), forAnd if only if, and M is present The transition relationship represents that pop domain R_ilMiddle stack character is a, and θ (a) ∈ I item, Carry out structural domain R_il′.Specific steps are described as follows：

● pop domain R_ilWith domain R_i(l-1), obtain domain R_ilIn item

● domain R_(l-1)In the clock value of all add θ (├^·), obtain domain R_i(l-1)′；

● pass through R_ilAnd R_i(l-1)' obtain domain R_il', R_il' item is respectively：Common stack character item comes from domain R_i(l-1)′；Commonly Clock item, global variable item come from domain R_il；Entry all is from domain R_i(l-1)′；

● stacking domain R_il', it is transformed into new state p '.

6) whenWhen, forExist in and if only if M The transition relationship represents, creates new thread and carrys out structural domain R_l′.Assuming that TDPN models, pushed away under dynamic creation is new and be The stack numbering of system is n+1.Specific execution step is as follows：

● pop domain R_l, the clock equivalence optimisation technique based on key point, general character item can be obtainedEntry

● itemWithAdd domain R_l, Obtain domain R_l', and stacking, it is transformed into new state p '.

Present invention research is based on network (Time Dynamic Pushdown Networks, TDPN) of being pushed net under time dynamic, For the Real-time and Concurrent recusive modeling for describing to create containing recurrence, dynamic thread.Description continuous time is introduced first in DPN Global clock, and the real number clock with time correlation global variable and stack character " age " can be described, so as to based on altogether Enjoy internal memory and carry out asynchronous communication, and be modeled with the Real-time and Concurrent system that dynamic thread creates.Secondly to being drawn based on integer The clock equivalent technique divided, provide a kind of optimisation technique based on clock key point, reduction clock section, after reducing conversion State space.For further reduced state space, using the dynamic converting method for being concerned only with stack top, by continuous model TDPN Corresponding DPN is converted into, while provides corresponding transfer algorithm.Then prove its conversion correctness and TDPN up to uniformity, So as to solve TDPN Reachability question up to technology using existing DPN.

Brief description of the drawings

Fig. 1 is x_i, x_jClock equivalence section.

Embodiment

The present invention proposes a kind of analysis method of reachability for being directed to and network model being pushed away under time dynamic, under time dynamic Network model is pushed away, using the clock equivalence optimisation technique based on key point, dynamically by network mould of being pushed net under continuous time dynamic Type is converted to and pushes away network model under discrete dynamic, so as to what is solved to the accessibility problem that network model is pushed away under time dynamic A kind of automatic mode.

First, the TDPN model stages are constructed：TDPN models are a kind of extension of DPN models, and basic thought is to be introduced in DPN The real-time clock of description continuous time, for describing the Real-time and Concurrent recursive program with dynamic thread creation.

Set out by TMPDN syntax and semantics, the conversion method that Real-time and Concurrent Program transformation is TMPDN is divided into stack Migrate switch transition between conversion, stack and concurrently perform three classes of conversion.

1st, concurrent program abstract model --- network of being pushed net under time dynamic is built

TDPN models are a four-tuple T=(P, Γ, Δ, X), wherein：P is state set；Γ is stack character set；Δ= Δ_nop∪Δ₌∪Δ_├∪Δ_push∪Δ_pop∪Δ_dcIt is migration rules set, wherein Δ_nopRepresent do-nothing operation migration, Δ₌Represent Clock assignment migrates, Δ_├Represent time passage migration, Δ_pushRepresent stacking migration, Δ_popExpression is popped migration, Δ_dcRepresent dynamic State thread creation migrates；X represents clock collection, its value function Represent forIt is θ in current value (x) it is, also similar therewith with the global variable and stack character " age " value of time correlation.

When TDPN models migrate, multiple lower pushing systems concurrently perform, i.e., synchronization has multiple stacks to be migrated.It is assumed that G is global variable collection, and TDPN general layouts are represented by：Wherein：Represent current global variable g and its " age " θ (g) two tuples<g,θ(g)>；p_i∈ P represent local state Node,Represent the stack content ω that stack sequence is i_iWith its " age " θ (ω_i) two tuples<ω_i,θ(ω_i)>；Represent clock X and its value θ (x) two tuples<x,θ(x)>.TDPN migration behavior aggregate op includes do-nothing operation nop；Clock resetting x ← I, its Middle x ∈ X, I represent clock span；Time passage Time ← v, wherein Time represent the time of passage, and v represents specific and passed Real number value, in the case of no ambiguity the present invention with θ+v represent clock value increase v；Stack-incoming operation push (a, I), represent into Stack character a, and belong to section I real number to its age assignment；Pop operations pop (a, I), first judge stack symbol a " age " Whether meet section I, carry out Pop operations if meeting, otherwise do not perform operation；Dynamic thread creates operationRepresent dynamic State creates a new thread.

2nd, TDPN operational semantics

For convenience, when general layout migrates, the only migration of one lower pushing system of description performs, and its remaining pushing system is not Become, the situation that multiple lower pushing systems concurrently perform is also similar therewith, and the operational semantics of TDPN general layout transition relationships is defined as follows：

1) Δ=Δ_nopWhen, op=nop,Represent that general layout interior element does not change；

2) Δ=Δ₌When, op=x ← I,c∈I；It is represented to clock x and specifies I scopes Interior arbitrary value v, other general layout interior elements do not change；

3) Δ=Δ_├When, op=Time ← c,Assuming thatSoAll clocks increase v in general layout are represented, when non-in general layout Clock content does not change；

4) Δ=Δ_pushWhen, op=push (a, I),V ∈ I,Variable a is pressed into by expression Stack top, and corresponding clock is set as x, its clock value is the arbitrary value in the range of I；

5) Δ=Δ_popWhen, op=pop (a, I),V ∈ I,Represent stack top internal clock value Ejected for the variable a of I scopes；

6) Δ=Δ_dcWhen, op=dc,Represent to create new thread stack content.

2nd, the conversion method design phase：In order to analyze TDPN accessibility, it need to be abstracted, reduce its state sky Between, the clock equivalence optimisation technique of the invention based on key point, using on-the-fly thought, only it is concerned about the conversion of stack top, Dynamically continuous model is abstracted and is converted into discrete DPN models, then using existing DPN reachability analysis technology, so as to solve TDPN Reachability question.

In order to reduce the division of state space, first reduced time region after conversion, the clock based on key point is of equal value Optimisation technique compared with integer partitioning region, can allow conversion after state space exponential reduction.Secondly based on the technology, TDPN In model with continuous time correlated variables -- global variable and its " age ", stack character and its " age ", clock variable and its take Value, be converted to the domain of DPN stack content described in DPN models.

Continuous time discrete time will be converted to using clock equivalent technique, general layout will be migrated using the thought of dynamic translation Change, finished until all general layouts calculate one by one.

1st, based on crucial Dot Clock optimisation technique

In order to describe to be converted into the general layout of DPN systems, domain R concept is introduced, domain R is made up of one group of item r, and item r is It is made up of character set Z and set of keypoints key.

Character set Z includes general character collection Y and record character set Y^·, it is described as Z=Y ∪ Y^·.Wherein general character JiYBao Include：(1) clock collection X；(2) stack character Γ；(3) global variable collection G；(4) reference clock character ├, for recording time passage, Not so it is always 0, therefore general character collection Y can be described as Y=X ∪ Γ ∪ G ∪ { ├ } unless carrying out Pop operations.Record character Collect Y^·General character Y time passage is represented, if X^·={ x^·| x ∈ X } represent record global clock；Γ^·={ a^·| a ∈ Γ } table Show recording stack character；G^·={ g^·| g ∈ G } represent record global variable；{├^·Record reference clock character set is represented, it is main next Time passage is recorded, so as to renewal time during Pop operations, therefore character set is recorded and is described as Y^·=X^·∪Γ^·∪G^·∪{├^·}。

For the character set arbitrarily with time correlation, its time-shift is determined by some key points, and has maximum Value, therefore can be to any character, can each self-defined and maximum constant k of time correlation_Max, it is all to be more than k_MaxAll with symbol ∞ come Represent.To any character z_i∈ Z, the migration changed according to the time, the time-critical point for determining migration, therefore character z can be found_i's Time-critical point set key_i={ 0, k_i1..., k_il..., k_im, k_iMax, ∞ }, wherein 1<l<M, 1<i≤|Z|.According to above-mentioned character Collection and crucial point set, can obtain domain

Clock equivalence optimisation technique is exactly continuous clock value discretization, i.e. real number clock valueDivision For two parts：(1) key point partExpression takes downwards key point to real number value x；(2) remainder

Assuming that x ∈ X are any clock element in TDPN, clock x real number value is represented with θ (x),During expression pair Clock x carries out domain equivalence, takes key point part.Assuming that for any two clock x_i, x_j∈ X, when the clock for meeting following rule Value, then be clock of equal value：

(1)θ(x_i)>k_iMaxAnd if only ifThat is x_iClock value be more than maximum, x_iTake infinitely great ∞.

(2)k_il≤θ(x_i)<k_i(l+1)And if only ifThat is x_iClock value be less than key point k_i(l+1)And it is more than Equal to k_ilWhen, x_iTake key point k_il。

(3) assumeAnd if only if re (θ (x_i)<re(θ (x_j)), i.e. x_iTake key point k_il, x_jTake key point k_jl, work as x_iClock value and key point k_ilDifference be less than x_jClock value with Key point k_jlDifference when, be denoted as re (x_i)<re(x_j)。

Assuming that for any two clock x_i, x_j∈ X and key={ key₁..., key_n, the clock based on clock key point Domain rule of equal value.For example (0≤θ (x_i)<k_i1, 0≤θ (x_j)<k_j1) region, And re (θ (x_i)) >re(θ(x_j))；In (k_i1≤θ(x_i)<k_i2, k_j1≤θ(x_j)<k_j2) region, And re (θ (x_i))<re(θ(x_j)), then the clock value in section is clock of equal value, dash area as shown in Figure 1.

2nd, structural transform rule

For further reduced state space, using on-the-fly technologies and with dynamic translation thought, stack top is concerned only with And next layer of domain is changed, without being concerned about stack other parts, then according to different migrations, different switching rule is provided, so as to The TDPN accessibility problems of complexity can be converted to DPN accessibility problems.

It is DPN M=(P by T dynamic translations assuming that giving a TDPN T=(P, Γ, Δ, X)^M, Γ^M, Δ^M), to P^M, Γ^M, Δ^MIt is as follows to carry out dynamic transition rules：

(I) state set P^M：That is P^M=P.

(II) stack character setIf a ∈ { Γ, ├ }, thenAnd

(III) transition relationship Δ^MConstruction：

Assuming that the TDPN currently containing n stack, for convenience, only describes the lower pushing system that sequence is i and performs pop down And Pop operations, other stack operations are similar therewith.If the stack level of the lower pushing system is l, and stack bottom numbering is 1, stack top numbering For l.The TDPN contains global variable g, clock variable x, stack content ω={ ω₁…ω_i…ω_n, wherein ω_iRepresent to push away under No. i The stack content of system, uses ω_il|ΓRepresent ω_iIt is projected in Γ stack top character.Each table Show its key point of " age " and value under clock equivalence.It is corresponding in M present clock equivalence domain so as to understand WhereinRepresentative domain R_lRecord stack top character, ├ tables Show domain R_lReference clock character, ├^·Representative domain R_lCorresponding time passage character.

TDPN general layoutsφ=(γ, op, γ ') ∈ Δs represent T general layout migration, corresponding M lattice Office's migration is represented byWherein p and p ' is identical with state in T, before and after representing that general layout migrates respectively State；R_l={ R_1l…R_il…R_nlRepresent stack top domain, wherein R_ilRepresent the stack top domain of No. i lower pushing system, R_lAnd R_l' difference table Show the front and rear stack top domain of general layout migration；Action migration collection op ' corresponds to T op, below main description constructed according to different op R_l′：

(1) as op=nop, forExist in and if only if M State is only changed in T hollow operations, so general layout migration also only changes state, domain R in M_l Keep constant.

(2) as op=(x ← I), forExist in and if only if M The transition relationship is represented to DPN domains R_lThe item that middle clock is x performsBehaviour Make, wherein θ (x) ' ∈ I, carry out structural domain R_l′.Specific implementation procedure is as follows：

● domain R_lPop, obtain R_lIn itemIt is θ (x) ' to reset θ (x), forms new item

● itemInstead of domain R_lIn itemObtain domain R_l', and stacking, it is transformed into new state p′。

(3) as op=(Time ← v), forExist in and if only if M Transition relationship representative domain R_lIn except reference clock item (├, 0), remaining all when Clock value carrys out structural domain R plus time passage v_l ⁺.Specifically performing step is：

● domain R_lPop, except reference clock, all passed v plus the time, Expression corresponds to g, ω_il, x new general term,Respectively Corresponding new record item is represented,Represent reference clock entry；

● new item replaces original item, obtains domain R_l ⁺, and stacking, it is transformed into new state p '.

(4) as op=push (a, I), forAnd if only if, and M is present The transition relationship represents, carries out stack-incoming operation to No. i lower pushing system, is by character A, is worth and isItem stacking domain R_il, carry out structural domain R_i(l+1).Detailed process is as follows：

● from R_ilObtain itemWith

●Respectively instead of Obtain domain R_i(l+1), and stacking, it is transformed into new state p '.

(5) as op=pop (a, I), forAnd if only if, and M is present The transition relationship represents that pop domain R_ilMiddle stack character is a, and θ (a) ∈ I item, Carry out structural domain R_il′.Specific steps are described as follows：

● pop domain R_ilWith domain R_i(l-1), obtain domain R_ilIn item

● domain R_(l-1)In the clock value of all add θ (├^·), obtain domain R_i(l-1)′；

● pass through R_ilAnd R_i(l-1)' obtain domain R_il', R_il' item is respectively：Common stack character item comes from domain R_i(l-1)′；Commonly Clock item, global variable item come from domain R_il；Entry all is from domain R_i(l-1)′；

● stacking domain R_il', it is transformed into new state p '.

(6) whenWhen, forExist in and if only if M The transition relationship represents, creates new thread and carrys out structural domain R_l′.Assuming that TDPN models, pushed away under dynamic creation is new and be The stack numbering of system is n+1.Specific execution step is as follows：

● pop domain R_l, the clock equivalence optimisation technique based on key point, general character item can be obtainedEntry

● itemWithAdd domain R_l, Obtain domain R_l', and stacking, it is transformed into new state p '.

3rd, in the algorithm design phase：Based on clock optimization of equal value and dynamic translation thought, propose that one kind is directed to TDPN T= (P, Γ, Δ, X) is converted to DPN M=(P^M, Γ^M, Δ^M) algorithm, the algorithm be directed to T transition relationship Δ, pass through change rule Then, transition relationship Δ corresponding to M is exhaustively calculated^M。

Based on clock optimization of equal value and dynamic translation thought, propose to be converted to DPN M for TDPN T=(P, Γ, Δ, X) =(P^M, Γ^M, Δ^M) algorithm, the algorithm be directed to T transition relationship Δ, by the transformation rule of upper section, exhaustively calculate in M Corresponding transition relationship Δ^M.The input of algorithm is continuous TDPN T, and output is discrete DPN M.Assuming that TDPN initial lattice Office beEach stack content is initially sky, corresponding to construct M initial domains R_init。

If T transition relationship set has φ=(γ, op, γ ') ∈ Δs, its general layout includes global variableStack character StringClockM current general layout be β=<p,R_l>, domain R_lComprising (├, 0) represents g, ω_il, general term corresponding to x, ├, Represent corresponding entry.According to φ and R_lCan dynamic structural domain R_l', that is, transition relationship be present The transition relationship is added to Δ^MIn.

Algorithm：TDPN is converted into DPN algorithms

Input：TDPN T=(P, Γ, Δ, X)

Output：Corresponding DPN M=(P^M, Γ^M, Δ^M)

The 1st and 2 rows represent the general layout to worker thread and the initialization in domain respectively in transfer algorithm, since the 4th row, pin To T general layout transition relationship Δ, limit calculates the transition relationship Δ that domain representation is used in M^M.Wherein the 8th and 9 rows represent do-nothing operation Migration, corresponding M only change state, and domain is constant.10th to 12 row describes clock resetting operation migration, domain R_lIn clock x valueReset to13rd to 15 row describes time passage migration, domain R_lIn remove reference clock item (├, 0), remaining institute There is the clock value of item, all plus time passage v.16th to 18 row describes stack-incoming operation migration, press-in character a.19th to 22 Row description Pop operations migration, wherein R_i(l-1)' representative domain R_i(l-1)All items all add domain R_ilTime passage θ (├^·).23rd Dynamic creation thread migration is described to 25 rows, the new thread of establishment is n+1.For TDPN T, the algorithm is terminable, and should The time complexity of algorithm, had exponent relation with the cartesian product of item character set and crucial point set, with the size of program exponentially Relation.

For TDPN T, the algorithm is terminable, and the time complexity of the algorithm, with item character set and crucial point set Cartesian product have exponent relation, had exponent relation with the size of program.

4th, Reachability question proves the stage：By proving state p_FUp to and if only if its transition status p in TDPN_F′ It is reachable in DPN, so that it is determined that model conversion whether there is mistake.

TDNP Reachability questions are changed into DPN Reachability questions by clock equivalence optimisation technique, need to prove to convert from T Into M correctness, i.e. state p_FIn TDPN up to and if only if its transition status p_F' reachable in DPN.

Define 1 (accessibility):If migratory system TDPN T,For T initial lattice Office, whereinFor global variable initial value；p_initFor original state；ε is stack initial value (representing that stack is empty)；For it is initial when Clock (is entered as 0), target patternIf there is general layout migration in TThat State p_FIt is reachable in T.

If R=R₀R₁…R_nIt is one group of domain that M stacks domain collection closes.For R₁、R₂Two domains, if R₁It is R₂Strict partial order is closed System, remembersIf R₁It is R₂Non-critical partial ordering relation, remembersFor domain collection R, ifThen R is referred to as the domain of dependence, ifThen R is referred to as the weak domain of dependence.If R is (weak) domain of dependence, Then general layout β=<P, R>For (weak) related general layout.For weak domain of dependence R=R₀R₁…R_nWith domain R '=R₀′R₁′…R_n', if R_n′ =R_n、R_i′∈R_i ⁺(wherein R_i ⁺It is R_iTime-shift domain) andThen domain R^′It is domain R Strong correlation domain.Given one related general layout β in M=<P, R>If domain R ' is domain R strong correlation domain, general layout β '=<P, R′>It is exactly β strong correlation general layout.

Theorem 1：For T any one general layout γ, converted by the way that clock is of equal value, corresponding general layout β all be present in M.

Prove：If a M general layout β=<P, R>, a T general layoutWhereinAssuming that S is that variables collection, S are converted into the domain R in M through clock domain equivalence to migratory system T this moment.IfR=R₀R₁…R_nWith S value θ (i.e. θ_|=S), expression is set up：

● p '=p

●

●

So γ |=_Sβ, i.e., for T any one general layout γ, by clock zone it is encoded translated after, all exist therewith in M Corresponding general layout β.

Prove that accessibility need to first introduce following two law：

Law 1：For belonging to M any one canonical up to general layout β, β strong correlation general layout β '=<P, R '>, S be T this Variables collection is carved, there will necessarily be in T therewith for general layout γ, γ be present |=_Sβ and

Law 2：Any one general layout γ for belonging to T, there will necessarily be corresponding pattern β, at least in the presence of a β in M Strong correlation general layout β '=<P, R '>, and existence domain R ' conversion set S, then γ be present |=_Sβ and

Theorem 2：State p_FIn TDPN T up to and if only if p_F' reachable in DPN M.

Prove：First demonstrate,prove adequacy：State p_FIt is reachable in TDPNIts transition status p_F' reachable in DPN.

If dbjective state p_F' in M it is reachable, then a canonical is there is up to general layout β (p_F' the shape for being general layout β State).Because all reachable general layouts of DPN M are all weak correlations, you can up to general layout β be weak related general layout, therefore at least have one Corresponding strong correlation general layout β '=<P, R '>.A canonical general layout β in migratory system M is understood by law 1, a strong phase be present The obstruction and rejection office β ' and set S for being converted into R ', corresponding pattern γ therewith is there will necessarily be in T, γ be present |=_Sβ andThat is state p_F(p_FFor general layout γ state) it is reachable in T.

Necessity is demonstrate,proved again：State p_FIt is reachable in TDPNIts transition status p_F' reachable in DPN.

If dbjective state p_F' it is reachable in T, understand to there will necessarily be therewith for general layout β (p in M by theorem 1_F' it is lattice Office β state), therefore at least exist a strong correlation general layout β '=<P, R '>.At one of migratory system T knowable to law 2 General layout γ, a strong correlation general layout β ' be present and be converted into R ' domain set S, corresponding pattern β therewith is there will necessarily be in M, is deposited In γ |=_Sβ andThat is state p_F′(p_F' the state for being general layout β) it is reachable in M.

Therefore, state p_FIn TDPN up to and if only if its transition status p_F' reachable in DPN.

Design mistake present in concurrent recursive program or leak can be found out by above method step, ensure program Reliability and correctness.This method is the accessibility method for solving of automation, it is possible to achieve network of being pushed net under time dynamic is reachable Sex chromosome mosaicism can determine that solution, excessively be participated in without user, simple, effective up to general layout calculating process.

Claims (1)

1. the conversion method for network of being pushed net under time dynamic, it is characterized in that, comprise the following steps：

Real-time and Concurrent recursive program is converted to network of being pushed net under a time dynamic by step (1)；

The abstract model of step (1.1) construction Real-time and Concurrent recursive program is network of being pushed net under time dynamic；

Network of being pushed net under the time dynamic constructed is a four-tuple T=(P, Γ, Δ, X), and wherein P is state set；Γ is stack word Symbol collection；Δ=Δ_nop∪ Δs=∪ Δs_├∪Δ_push∪Δ_pop∪Δ_dcIt is migration rules set, wherein Δ_nopRepresent that do-nothing operation is moved Move, Δ=expression clock assignment migration, Δ_├Represent time passage migration, Δ_pushRepresent stacking migration, Δ_popExpression, which is popped, moves Move, Δ_dcRepresent that dynamic thread creates migration；X represents clock collection, its value functionRepresent forWorking as Preceding value is θ (x)；

Network situation is pushed away under institute's build time dynamicThe state of the model at a time is represented, its In：Represent current global variable g and its age θ (g) two tuples<g,θ(g)>；p_i∈ P represent local state node,Represent the stack content that stack sequence is i ω_iWith its age θ (ω_i) two tuples<ω_i,θ(ω_i)>；Represent clock x and its value θ (x) two tuples<x,θ(x)>；

Network of being pushed net under the time dynamic constructed is described step (1.2) with operational semantics；

Push net under time dynamic model of the network as real-time multithread program, moved for describing multiple lower pushing systems while producing Move, its transition relationship Δ=Δ_nop∪ Δs=∪ Δs_├∪Δ_push∪Δ_pop∪Δ_dcGiven below according to different migration action op Go out it and perform implication；

1) Δ=Δ_nopWhen, op=nop,Represent that general layout interior element does not change；

2) Δ=Δ=when, op=x ← I,v∈I；Clock x is represented to specify in the range of I Arbitrary value v, other general layout interior elements do not change；

3) Δ=Δ_├When, op=Time ← c,Assuming thatSoAll clocks increase v in general layout are represented, when non-in general layout Clock content does not change；

4) Δ=Δ_pushWhen, op=push (a, I),V ∈ I,Represent variable a being pressed into stack top, and Corresponding clock is set as x, its clock value is the arbitrary value in the range of I；

5) Δ=Δ_popWhen, op=pop (a, I),V ∈ I,Represent stack top internal clock value to be I models The variable a ejections enclosed；

6) Δ=Δ_dcWhen,Represent establishment new thread dc stack content

Push net network T=(P, Γ, Δ, X) under the time dynamic that step (2) is obtained step (1), is turned by following conversion methods Network M=(the P that push net are changed under dynamic^M,Γ^M,Δ^M)；

Step (2.1) state P^MConversion：I.e. T state set is identical with M state set；

Step (2.2) stack character setConversion：If a ∈ { Γ, ├ }, thenAndWherein a^·Represent recording stack character a time passage, symbolExpression rounds downwards；

Step (2.3) transition relationship Δ is to Δ^MTransformation rule；

If the stack level of the lower pushing system is l, and stack bottom numbering is 1, and stack top numbering is l；Push net network i.e. TDPN under time dynamic Contain global variable g, clock variable x, stack content ω={ ω₁…ω_i…ω_n, wherein ω_iIn the stack for representing No. i lower pushing system Hold, use ω_il|ΓRepresent ω_iIt is projected in Γ stack top character；Respectively represent its age and Key point of the value under clock equivalence；It is corresponding in M present clock equivalence domain so as to understand WhereinRepresentative domain R_lRecord stack top character, ├ tables Show domain R_lReference clock character, ├^·Representative domain R_lCorresponding time passage character；

TDPN general layoutsφ=(γ, op, γ ') ∈ Δs represent T general layout migration, and corresponding M general layout is moved Shifting is represented byWherein p and p ' is identical with state in T, represents the front and rear shape of general layout migration respectively State；R_l={ R_1l…R_il…R_nlRepresent stack top domain, wherein R_ilRepresent the stack top domain of No. i lower pushing system, R_lAnd R_l' lattice are represented respectively The front and rear stack top domain of office's migration；Action migration collection op ' corresponds to T op, and description below constructs R according to different op_l′：

1) as op=nop, forExist in and if only if M State is only changed in T hollow operations, so general layout migration also only changes state, domain R in M_lKeep constant；

2) as op=(x ← I), forExist in and if only if M The transition relationship is represented to DPN domains R_lThe item that middle clock is x performsOperation, Wherein θ (x) ' ∈ I, carry out structural domain R_l′；Specific implementation procedure is as follows：

Domain R_lPop, obtain R_lIn itemIt is θ (x) ' to reset θ (x), forms new item

Instead of domain R_lIn itemObtain domain R_l', and stacking, it is transformed into new state p '；

3) as op=(Time ← v), forExist in and if only if MTransition relationship representative domain R_lIn except reference clock item (├, 0), remaining all Clock value carrys out structural domain R plus time passage v_l ⁺；Specifically performing step is：

Domain R_lPop, except reference clock, all passed v plus the time, Expression corresponds to g, ω_il, x new general term,Respectively Corresponding new record item is represented,Represent reference clock entry；

New item replaces original item, obtains domain R_l ⁺, and stacking, it is transformed into new state p '；

4) as op=push (a, I), forAnd if only if, and M is presentThe transition relationship is represented, stack-incoming operation is carried out to No. i lower pushing system, will Character is a, is worth and isItem stacking domain R_il, carry out structural domain R_i(l+1)；Detailed process is as follows：

From R_ilObtain itemWith

Respectively instead of Obtain domain R_i(l+1), and stacking, it is transformed into new state p '；

5) as op=pop (a, I), forAnd if only if, and M is present The transition relationship represents that pop domain R_ilMiddle stack character is a, and θ (a) ∈ I , carry out structural domain R_il′；Specific steps are described as follows：

Pop domain R_ilWith domain R_i(l-1), obtain domain R_ilIn item

Domain R_(l-1)In the clock value of all add θ (├^·), obtain domain R_i(l-1)′；

Pass through R_ilAnd R_i(l-1)' obtain domain R_il', R_il' item is respectively：Common stack character item comes from domain R_i(l-1)′；Ordinary clock item, Global variable item comes from domain R_il；Entry all is from domain R_i(l-1)′；

Stacking domain R_il', it is transformed into new state p '；

6) as op=dc, forExist in and if only if M Should Transition relationship represents, creates new thread and carrys out structural domain R_l′；Assuming that TDPN models, it is n that dynamic creation, which newly descends the stack of pushing system to number, +1；Specific execution step is as follows：

Pop domain R_l, the clock equivalence optimisation technique based on key point, general character item can be obtained Entry

ItemWithAdd domain R_l, obtain Domain R_l', and stacking, it is transformed into new state p '.