CN105183652B - 时间动态下推网络的转换方法 - Google Patents

Abstract

本发明公开一种时间动态下推网络的转换方法，用于描述含有递归、动态线程创建的实时并发递归建模。首先在DPN中引入描述连续时间的全局时钟，以及能描述与时间相关全局变量和栈字符“年龄”的实数时钟，从而可对基于共享内存进行异步通信，且带有动态线程创建的实时并发系统进行建模。其次对基于整数划分的时钟等价技术，给出一种基于时钟关键点的优化技术，缩减时钟区间，从而缩减转换后的状态空间。由于时间动态下推网络为一种实时并发递归程序的抽象模型，基于关键点的时钟等价优化技术把该模型转换为动态下推网络，这样通过确认动态下推网络模型的执行是否会运行到错误状态，从而检测出此模型即所对应并发递归程序中的错误或漏洞。

Description

时间动态下推网络的转换方法

技术领域

本发明属于软件安全性和可靠性研究领域，涉及多线程并发递归程序的验证方法，是一种适用于含有时间的多线程并发递归程序抽象模型的可达性求解技术，具体涉及一种时间动态下推网络的转换方法。

背景技术

随着多核技术的发展，并发程序已成为当前程序设计研究的热点。由于并发执行存在不确定性，从而导致传统测试方法很难发现程序中隐匿的错误和漏洞。模型检验是一种通过穷尽搜索的自动化验证技术，已成为保证程序安全和可靠的重要手段，可作为测试方法的一种补充。可达性分析通过分析某一状态是否可达，是模型检验的重要核心技术。

近年来，研究人员基于自动机模型，引入实时时钟，用于描述实时系统建模及其验证。1994年Alur提出时间自动机(R.Alur，D.Dill，A theory of timed automata[J].Theoretical Computer Science，126(2)，pp.183-235，1994.)是在自动机的基础上引入描述连续时间的时钟，并给出了时钟等价技术，从而实现模型检验时间自动机(J.Bengtsson，W.Yi，Timed automata:Semantics，algorithms and tools[C]，4thAdvanced Course on Petri Nets，Eichstaat.Germany，pp.87-124，2004)。为了解决含有递归的实时系统建模，Trivedi(A.Trivedi，D.Wojtczak，Recursive Timed Automata[C]，ATVA 2010.LNCS，vol.6252，Springer，Heidelberg，pp.306–324.2010.)提出时间下推自动机，并通过时钟等价技术把时间下推自动机转换为下推自动机，解决最小时间花费的可达性问题。2013年Li(L G qiang，C X juan，O.Mizuhito，Nested Timed Automata[R]，Research report(School of Information Science，Japan Advanced Institute ofScience and Technology)，IS-RR-2013-004，pp.1-20，2013)提出了嵌套时间自动机，利用嵌套的思想来解决实时系统中的递归问题。但此类模型无法描述带有动态线程创建的实时并发系统建模。Bouajjani(A.Bouajjani，M.M.Olm，T.Touili.Regular symbolic analysisof dynamic networks of pushdown systems[C].Proceedings of the 16thInternational Conference on Concurrency Theory.LNCS 3653，San Francisco:CiscoSyst，2005，473-487.)提出一种并发下推系统(B.Bollig，D.Kuske，R.Mennicke，Thecomplexity of model checking multi-stack systems[C]，Proceedings ofthe201328th Annual ACM/IEEE Symposium on Logic in Computer Science，NewOrleans，LA，USA，pp.163-72，2013)的扩展模型——动态下推网络(DPN)，解决并发系统中新线程的动态创建，该模型适用于含有递归且带有动态线程创建的并发系统建模。基于DPN，Lammich(P.Lammich，M.M.Olm，H.Seidl，Contextual Locking for Dynamic PushdownNetworks[C].Static Analysis.Proceedings of 20th International Symposium，Seattle，WA，USA，pp.47-98，2013.)提出了上下文锁的技术，解决进程递归之间同步问题，并进行了逆向可达分析。Wenner(A.Wenner，Weighted dynamic pushdown networks[C]，19th European symposium on programming，Paphos，Cyprus，pp.590-609，2010.)在DPN中引入权值，用来求解最短路径的可达性。

由于上述模型无法描述实时多线程并发递归系统中线程间交互的情况，对于实时多线程并发递归程序而言，形式化验证此类程序将产生状态空间爆炸问题，给验证带来了极大困难。

发明内容

本发明所要解决的技术问题是提供一种时间动态下推网络的转换方法，其时间动态下推网络为一种实时并发递归程序的抽象模型，基于关键点的时钟等价优化技术把该模型转换为动态下推网络，这样通过确认动态下推网络模型的执行是否会运行到错误状态，从而检测出此模型即所对应并发递归程序中的错误或漏洞。

为解决上述问题，本发明是通过以下技术方案实现的：

时间动态下推网络的转换方法，包括如下步骤：

步骤(1)把所述的实时并发递归程序转换为一个时间动态下推网络。

步骤(1.1)构造实时并发递归程序的抽象模型即时间动态下推网络。

所构造的时间动态下推网络是一个四元组T＝(P，Γ，Δ，X)，其中：P是状态集；Γ是栈字符集；Δ＝Δ_nop∪Δ_＝∪Δ_├∪Δ_push∪Δ_pop∪Δ_dc是迁移规则集合，其中Δ_nop表示空操作迁移，Δ_＝表示时钟赋值迁移，Δ_├表示时间流逝迁移，Δ_push表示入栈迁移，Δ_pop表示出栈迁移，Δ_dc表示动态线程创建迁移；X表示时钟集，其取值函数表示对于在当前取值为θ(x)，与时间相关的全局变量和栈字符“年龄”取值亦与之类似。

所构造时间动态下推网络格局表示所述模型在某一时刻的状态，其中：表示当前全局变量g和其“年龄”θ(g)的二元组<g,θ(g)>；p_i∈P表示局部状态节点，表示栈序列为i的栈内容ω_i和其“年龄”θ(ω_i)的二元组<ω_i,θ(ω_i)>；表示时钟x和其取值θ(x)的二元组<x,θ(x)>。

步骤(1.2)将所构造的时间动态下推网络用操作语义进行描述。

时间动态下推网络作为实时多线程程序的模型，用于描述多个下推系统同时产生迁移，其迁移关系Δ＝Δ_nop∪Δ_＝∪Δ_├∪Δ_push∪Δ_pop∪Δ_dc下面根据不同的迁移动作给出其执行含义；

1)Δ＝Δ_nop时，op＝nop，表示格局内元素未发生变化；

2)Δ＝Δ_＝时，op＝x←I，c∈I；表示给时钟x指定I范围内的任意值v，其它格局内元素未发生变化；

3)Δ＝Δ_├时，op＝Time←c，假设那么表示格局内所有时钟增加v，格局内非时钟内容未发生变化；

4)Δ＝Δ_push时，op＝push(a,I)，v∈I，表示将变量a压入栈顶，并设定相应时钟为x，其时钟值为I范围内的任意值；

5)Δ＝Δ_pop时，op＝pop(a,I)，v∈I，表示将栈顶内时钟值为I范围的变量a弹出；

6)Δ＝Δ_dc时，op＝dc,表示创建新线程栈内容。

步骤(2)将步骤(1)所获得的时间动态下推网络T＝(P,Γ,Δ,X)，通过下述转换方法转换为动态下推网络M＝(P^M,Γ^M,Δ^M)；

步骤(2.1)状态P^M的转换：即T的状态集与M的状态集相同。

步骤(2.2)栈字符集的转换：若a∈{Γ,├},则且

步骤(2.3)迁移关系Δ到Δ^M的转换规则。

假设当前含有n个栈的TDPN，为了描述方便，仅描述序列为i的下推系统执行压栈和出栈操作，其它栈操作与之类似。设该下推系统的栈深度为l，且栈底编号为1，栈顶编号为l。该TDPN含有全局变量g，时钟变量x，栈内容ω＝{ω₁…ω_i…ω_n}，其中ω_i表示i号下推系统的栈内容，用ω_il|Γ表示ω_i投影在Γ的栈顶字符。各表示其“年龄”和取值在时钟等价下的关键点。从而可知对应在M的当前时钟等价域 其中表示域R_l记录栈顶字符，├表示域R_l的参考时钟字符，├^·表示域R_l对应的时间流逝字符。

TDPN格局φ＝(γ,op,γ′)∈Δ表示T的格局迁移，对应M的格局迁移可表示为其中p和p′与T中状态相同，分别表示格局迁移前后的状态；R_l＝{R_1l…R_il…R_nl}表示栈顶域，其中R_il表示i号下推系统的栈顶域，R_l和R_l′分别表示格局迁移前后的栈顶域；动作迁移集op′对应于T的op，下面主要描述根据不同的op构造R_l′：

1)当op＝nop时，对于当且仅当M中存在 在T中空操作只改变了状态，所以在M中格局迁移也只改变状态，域R_l保持不变。

2)当op＝(x←I)时，对于当且仅当M中存在 该迁移关系表示对DPN域R_l中时钟为x的项执行操作，其中θ(x)′∈I，来构造域R_l′。具体执行过程如下：

●域R_l出栈，获得R_l里的项重置θ(x)为θ(x)′，形成新项

●项代替域R_l中的项获得域R_l′，并入栈，转换到新的状态p′。

3)当op＝(Time←v)时，对于当且仅当M中存在 该迁移关系表示域R_l中除了参考时钟项(├，0)，其余所有项的时钟值加上时间流逝v，来构造域R_l ⁺。具体执行步骤为：

●域R_l出栈，除了参考时钟，全部加上时间流逝v， 表示对应于g、ω_il、x的新普通项，各表示相应的新记录项，表示参考时钟记录项；

●新项代替原来项，得到域R_l ⁺，并入栈，转换到新的状态p′。

4)当op＝push(a,I)时，对于当且仅当M存在 该迁移关系表示，对i号下推系统进行入栈操作，将字符为a，值为的项入栈域R_il，来构造域R_i(l+1)。具体过程如下：

●从R_il获得项和

●分别代替 获得域R_i(l+1)，并入栈，转换到新的状态p′。

5)当op＝pop(a,I)时，对于当且仅当M存在 该迁移关系表示，出栈域R_il中栈字符为a，且θ(a)∈I的项，来构造域R_il′。具体步骤描述如下：

●出栈域R_il和域R_i(l-1)，获得域R_il里的项

●域R_(l-1)中所有项的时钟值加上θ(├^·)，获得域R_i(l-1)′；

●通过R_il和R_i(l-1)′获得域R_il′，R_il′项分别为：普通栈字符项来自域R_i(l-1)′；普通时钟项、全局变量项来自域R_il；记录项全部来自域R_i(l-1)′；

●入栈域R_il′，转换到新的状态p′。

6)当时，对于当且仅当M中存在 该迁移关系表示，创建新线程来构造域R_l′。假设TDPN模型，动态创建新下推系统的栈编号为n+1。具体执行步骤如下：

●出栈域R_l，基于关键点的时钟等价优化技术，可得普通字符项记录项

●把项和加入域R_l，得到域R_l′，并入栈，转换到新的状态p′。

本发明研究基于时间动态下推网络(Time Dynamic Pushdown Networks，TDPN)，用于描述含有递归、动态线程创建的实时并发递归建模。首先在DPN中引入描述连续时间的全局时钟，以及能描述与时间相关全局变量和栈字符“年龄”的实数时钟，从而可对基于共享内存进行异步通信，且带有动态线程创建的实时并发系统进行建模。其次对基于整数划分的时钟等价技术，给出一种基于时钟关键点的优化技术，缩减时钟区间，从而缩减转换后的状态空间。为了进一步缩减状态空间，采用仅关注栈顶的动态转换方法，将连续模型TDPN转换成相应DPN，同时给出相应的转换算法。然后证明其转换的正确性及TDPN可达一致性，从而可利用现有的DPN可达技术解决TDPN的可达性问题。

附图说明

图1为x_i，x_j时钟等价区间。

具体实施方式

本发明提出一种针对时间动态下推网络模型的可达性分析方法，针对时间动态下推网络模型，采用基于关键点的时钟等价优化技术，动态地将连续的时间动态下推网络模型转换为离散的动态下推网络模型，从而对时间动态下推网络模型的可达问题进行求解的一种自动化方法。

一、构造TDPN模型阶段：TDPN模型为DPN模型的一种扩展，基本思想为在DPN中引入了描述连续时间的实时时钟，用来描述带动态线程创建的实时并发递归程序。

通过TMPDN的语法和语义出发，将实时并发程序转换为TMPDN的转换方法分为栈内迁移转换、栈间切换转换和并发执行转换三类。

1、构建并发程序抽象模型——时间动态下推网络

TDPN模型为一个四元组T＝(P，Γ，Δ，X)，其中：P是状态集；Γ是栈字符集；Δ＝Δ_nop∪Δ_＝∪Δ_├∪Δ_push∪Δ_pop∪Δ_dc是迁移规则集合，其中Δ_nop表示空操作迁移，Δ_＝表示时钟赋值迁移，Δ_├表示时间流逝迁移，Δ_push表示入栈迁移，Δ_pop表示出栈迁移，Δ_dc表示动态线程创建迁移；X表示时钟集，其取值函数 表示对于在当前取值为θ(x)，与时间相关的全局变量和栈字符“年龄”取值亦与之类似。

当TDPN模型迁移时，多个下推系统并发执行，即同一时刻有多个栈进行迁移。假定G为全局变量集，TDPN格局可表示为：其中：表示当前全局变量g和其“年龄”θ(g)的二元组<g,θ(g)>；p_i∈P表示局部状态节点，表示栈序列为i的栈内容ω_i和其“年龄”θ(ω_i)的二元组<ω_i,θ(ω_i)>；表示时钟x和其取值θ(x)的二元组<x,θ(x)>。TDPN的迁移动作集op包含空操作nop；时钟重置x←I，其中x∈X，I表示时钟取值范围；时间流逝Time←v，其中Time表示流逝的时间，v表示具体流逝的实数值，在没有歧义情况下本发明用θ+v表示时钟值增加v；入栈操作push(a,I)，表示入栈字符a，并且对其年龄赋值属于区间I的实数；出栈操作pop(a,I)，先判断栈符a的“年龄”是否满足区间I，如果满足则进行出栈操作，否则不执行操作；动态线程创建操作表示动态创建一个新线程。

2、TDPN的操作语义

为了描述方便，当格局迁移时，只描述一个下推系统的迁移执行，其余下推系统不变，多个下推系统并发执行的情况亦与之类似，TDPN格局迁移关系的操作语义定义如下：

1)Δ＝Δ_nop时，op＝nop，表示格局内元素未发生变化；

2)Δ＝Δ_＝时，op＝x←I，c∈I；表示给时钟x指定I范围内的任意值v，其它格局内元素未发生变化；

3)Δ＝Δ_├时，op＝Time←c，假设那么表示格局内所有时钟增加v，格局内非时钟内容未发生变化；

4)Δ＝Δ_push时，op＝push(a,I)，v∈I，表示将变量a压入栈顶，并设定相应时钟为x，其时钟值为I范围内的任意值；

5)Δ＝Δ_pop时，op＝pop(a,I)，v∈I，表示将栈顶内时钟值为I范围的变量a弹出；

6)Δ＝Δ_dc时，op＝dc,表示创建新线程栈内容。

二、转换方法设计阶段：为了分析TDPN的可达性，需对其进行抽象，缩减其状态空间，本发明基于关键点的时钟等价优化技术，使用on-the-fly的思想，仅关心栈顶的转换，动态地将连续模型抽象转换成离散DPN模型，然后使用现有DPN可达分析技术，从而解决TDPN的可达性问题。

为了缩减转换后的状态空间，首先缩减时间区域的划分，基于关键点的时钟等价优化技术与整数划分区域相比，可让转换后的状态空间指数缩减。其次基于该技术，把TDPN模型中与连续时间相关变量--全局变量及其“年龄”、栈字符及其“年龄”、时钟变量及其取值，转换为DPN模型中描述DPN的栈内容的域。

利用时钟等价技术将连续时间转换为离散时间，利用动态转换的思想对格局迁移逐条转换，直至所有格局计算完毕。

1、基于关键点时钟优化技术

为了描述转换成DPN系统的格局，引入域R的概念，域R是由一组项r组成，而项r是由字符集合Z和关键点集合key组成。

字符集Z包含普通字符集Y和记录字符集Y^·，描述为Z＝Y∪Y^·。其中普通字符集Y包括：(1)时钟集X；(2)栈字符Γ；(3)全局变量集G；(4)参考时钟字符├，用来记录时间流逝，除非进行出栈操作，不然始终为0，故普通字符集Y可描述为Y＝X∪Γ∪G∪{├}。记录字符集Y^·表示普通字符Y的时间流逝，设X^·＝{x^·|x∈X}表示记录全局时钟；Γ^·＝{a^·|a∈Γ}表示记录栈字符；G^·＝{g^·|g∈G}表示记录全局变量；{├^·}表示记录参考时钟字符集，主要来记录时间流逝，以便出栈操作时更新时间，故记录字符集描述为Y^·＝X^·∪Γ^·∪G^·∪{├^·}。

对于任意与时间相关的字符集，其时间迁移是由一些关键点所确定的，且有最大值，故可对任一字符，可各自定义与时间相关的最大值常量k_Max，所有大于k_Max都用符号∞来表示。对任意字符z_i∈Z，根据时间转换的迁移，可找到决定迁移的时间关键点，故字符z_i的时间关键点集key_i＝{0，k_i1，…，k_il，…，k_im，k_iMax，∞}，其中1<l<m，1<i≤|Z|。根据上述字符集和关键点集，可得域

时钟等价优化技术就是把连续时钟值离散化，即实数时钟值划分为两个部分：(1)关键点部分表示对实数值x向下取关键点；(2)剩余部分

假设x∈X为TDPN中的任意时钟元素，用θ(x)表示时钟x的实数值，表示对时钟x进行域等价，取关键点部分。假设对于任意两个时钟x_i，x_j∈X，当满足如下规则的时钟值，则为等价时钟：

(1)θ(x_i)>k_iMax当且仅当即x_i的时钟值大于最大值，x_i取无穷大∞。

(2)k_il≤θ(x_i)<k_i(l+1)当且仅当即x_i的时钟值小于关键点k_i(l+1)且大于等于k_il时，x_i取关键点k_il。

(3)假定当且仅当re(θ(x_i)<re(θ(x_j))，即x_i取关键点k_il，x_j取关键点k_jl，当x_i的时钟值与关键点k_il的差值小于x_j的时钟值与关键点k_jl的差值时，记作re(x_i)<re(x_j)。

假设对于任意两个时钟x_i，x_j∈X和key＝{key₁，…，key_n}，基于时钟关键点的时钟域等价规则。譬如(0≤θ(x_i)<k_i1，0≤θ(x_j)<k_j1)区域， 且re(θ(x_i))>re(θ(x_j))；在(k_i1≤θ(x_i)<k_i2，k_j1≤θ(x_j)<k_j2)区域， 且re(θ(x_i))<re(θ(x_j))，则区间内的时钟值为等价时钟，如图1所示的阴影部分。

2、构造转换规则

为了进一步缩减状态空间，采用on-the-fly技术和用动态转换思想，仅关注栈顶及下一层的域转换，而无需关心栈其它部分，然后根据不同迁移，给出不同转换规则，从而可将复杂的TDPN可达问题转换为DPN可达问题。

假设给定一个TDPN T＝(P，Γ，Δ，X)，将T动态转换为DPN M＝(P^M，Γ^M，Δ^M)，对P^M，Γ^M，Δ^M进行动态转换规则如下：

(Ⅰ)状态集P^M：即P^M＝P。

(Ⅱ)栈字符集若a∈{Γ，├}，则且

(Ⅲ)迁移关系Δ^M的构造：

假设当前含有n个栈的TDPN，为了描述方便，仅描述序列为i的下推系统执行压栈和出栈操作，其它栈操作与之类似。设该下推系统的栈深度为l，且栈底编号为1，栈顶编号为l。该TDPN含有全局变量g，时钟变量x，栈内容ω＝{ω₁…ω_i…ω_n}，其中ω_i表示i号下推系统的栈内容，用ω_il|Γ表示ω_i投影在Γ的栈顶字符。各表示其“年龄”和取值在时钟等价下的关键点。从而可知对应在M的当前时钟等价域 其中表示域R_l记录栈顶字符，├表示域R_l的参考时钟字符，├^·表示域R_l对应的时间流逝字符。

TDPN格局φ＝(γ,op,γ′)∈Δ表示T的格局迁移，对应M的格局迁移可表示为其中p和p′与T中状态相同，分别表示格局迁移前后的状态；R_l＝{R_1l…R_il…R_nl}表示栈顶域，其中R_il表示i号下推系统的栈顶域，R_l和R_l′分别表示格局迁移前后的栈顶域；动作迁移集op′对应于T的op，下面主要描述根据不同的op构造R_l′：

(1)当op＝nop时，对于当且仅当M中存在 在T中空操作只改变了状态，所以在M中格局迁移也只改变状态，域R_l保持不变。

(2)当op＝(x←I)时，对于当且仅当M中存在 该迁移关系表示对DPN域R_l中时钟为x的项执行操作，其中θ(x)′∈I，来构造域R_l′。具体执行过程如下：

●域R_l出栈，获得R_l里的项重置θ(x)为θ(x)′，形成新项

●项代替域R_l中的项获得域R_l′，并入栈，转换到新的状态p′。

(3)当op＝(Time←v)时，对于当且仅当M中存在 该迁移关系表示域R_l中除了参考时钟项(├，0)，其余所有项的时钟值加上时间流逝v，来构造域R_l ⁺。具体执行步骤为：

●域R_l出栈，除了参考时钟，全部加上时间流逝v， 表示对应于g、ω_il、x的新普通项，各表示相应的新记录项，表示参考时钟记录项；

●新项代替原来项，得到域R_l ⁺，并入栈，转换到新的状态p′。

(4)当op＝push(a,I)时，对于当且仅当M存在 该迁移关系表示，对i号下推系统进行入栈操作，将字符为a，值为的项入栈域R_il，来构造域R_i(l+1)。具体过程如下：

●从R_il获得项和

●分别代替 获得域R_i(l+1)，并入栈，转换到新的状态p′。

(5)当op＝pop(a,I)时，对于当且仅当M存在 该迁移关系表示，出栈域R_il中栈字符为a，且θ(a)∈I的项，来构造域R_il′。具体步骤描述如下：

●出栈域R_il和域R_i(l-1)，获得域R_il里的项

●域R_(l-1)中所有项的时钟值加上θ(├^·)，获得域R_i(l-1)′；

●通过R_il和R_i(l-1)′获得域R_il′，R_il′项分别为：普通栈字符项来自域R_i(l-1)′；普通时钟项、全局变量项来自域R_il；记录项全部来自域R_i(l-1)′；

●入栈域R_il′，转换到新的状态p′。

(6)当时，对于当且仅当M中存在 该迁移关系表示，创建新线程来构造域R_l′。假设TDPN模型，动态创建新下推系统的栈编号为n+1。具体执行步骤如下：

●出栈域R_l，基于关键点的时钟等价优化技术，可得普通字符项记录项

●把项和加入域R_l，得到域R_l′，并入栈，转换到新的状态p′。

三、在算法设计阶段：基于时钟等价优化和动态转换思想，提出一种针对TDPN T＝(P，Γ，Δ，X)转换为DPN M＝(P^M，Γ^M，Δ^M)的算法，该算法针对T的迁移关系Δ，通过转换规则，穷尽地计算M对应的迁移关系Δ^M。

基于时钟等价优化和动态转换思想，提出针对TDPN T＝(P，Γ，Δ，X)转换为DPN M＝(P^M，Γ^M，Δ^M)的算法，该算法针对T的迁移关系Δ，通过上节的转换规则，穷尽地计算在M对应的迁移关系Δ^M。算法的输入是连续的TDPN T，输出是离散的DPN M。假设TDPN的初始格局为每个栈内容初始都为空，对应构造M初始域R_init。

若T的迁移关系集合存在φ＝(γ,op,γ′)∈Δ，其格局包含全局变量栈字符串时钟M的当前格局为β＝<p,R_l>，域R_l包含 (├,0)表示g、ω_il、x、├对应的普通项， 表示相应的记录项。根据φ和R_l可动态构造域R_l′，即存在迁移关系将该迁移关系添加到Δ^M中。

算法：TDPN转化为DPN算法

输入：TDPN T＝(P，Γ，Δ，X)

输出：对应的DPN M＝(P^M，Γ^M，Δ^M)

转换算法中第1和2行分别表示对工作线程的格局和域的初始化，从第4行开始，针对T的格局迁移关系Δ，穷尽计算在M中用域表示的迁移关系Δ^M。其中第8和9行表示空操作迁移，对应M只改变状态，域不变。第10至12行描述时钟重置操作迁移，域R_l中的时钟x的值重置为第13至15行描述时间流逝迁移，域R_l中除参考时钟项(├，0)，其余所有项的时钟值，全部加上时间流逝v。第16至18行描述入栈操作迁移，压入字符a。第19至22行描述出栈操作迁移，其中R_i(l-1)′表示域R_i(l-1)所有项都加上域R_il的时间流逝θ(├^·)。第23至25行描述动态创建线程迁移，创建的新线程为n+1。对于TDPN T，该算法是可终止的，且该算法的时间复杂度，与项字符集和关键点集的笛卡尔积呈指数关系，与程序的大小呈指数关系。

对于TDPN T，该算法是可终止的，且该算法的时间复杂度，与项字符集和关键点集的笛卡尔积呈指数关系，与程序的大小呈指数关系。

四、可达性问题证明阶段：通过证明状态p_F在TDPN中可达当且仅当其转换状态p_F′在DPN中可达，从而确定模型转换是否存在错误。

把TDNP可达性问题通过时钟等价优化技术转化成DPN可达性问题，需证明从T转化成M的正确性，即状态p_F在TDPN可达当且仅当其转换状态p_F′在DPN可达。

定义1(可达性):设迁移系统TDPN T，为T的初始格局，其中为全局变量初始值；p_init为初始状态；ε为栈初始值(表示栈空)；为初始时钟(赋值为0)，目标格局如果T存在格局迁移那么状态p_F在T可达。

设R＝R₀R₁…R_n是M栈域集合上的一组域。对于R₁、R₂两个域，如果R₁是R₂严格偏序关系，记住如果R₁是R₂非严格偏序关系，记住对于域集R，如果则称R为相关域，如果则称R为弱相关域。如果R为(弱)相关域，则格局β＝<p，R>为(弱)相关格局。对于弱相关域R＝R₀R₁…R_n和域R′＝R₀′R₁′…R_n′，如果R_n′＝R_n、R_i′∈R_i ⁺(其中R_i ⁺是R_i的时间迁移域)、并且则域R^′是域R的强相关域。给定一个在M的相关格局β＝<p，R>，如果域R′是域R的强相关域，则格局β′＝<p，R′>就是β的强相关格局。

定理1：对于T任意一个格局γ，通过时钟等价转化，在M都存在与之对应的格局β。

证明：设M的一个格局β＝<p，R>，T的一个格局其中假设S为迁移系统T此刻变量集合，S经过时钟域等价转换成M中的域R。设R＝R₀R₁…R_n和S的值θ(即θ_|＝S)，下面表达式成立：

●p′＝p

●

●

那么γ|＝_Sβ，即对于T任意一个格局γ，通过时钟域编码转化后，在M都存在与之对应的格局β。

要证明可达性需先引入下面两个定律：

定律1：对于属于M的任意一个正则可达格局β，β的强相关格局β′＝<p，R′>，S为T此刻变量集合，在T里必定存在与之对于格局γ，存在γ|＝_Sβ并且

定律2：对于属于T的任意一个格局γ，在M里必定存在对应格局β，至少存在一个β的强相关格局β′＝<p，R′>，并且存在域R′的转换集合S，那么存在γ|＝_Sβ并且

定理2：状态p_F在TDPN T可达当且仅当p_F′在DPN M可达。

证明：先证充分性：状态p_F在TDPN可达其转换状态p_F′在DPN可达。

如果目标状态p_F′在M是可达，那么就存在一个正则可达格局β(p_F′为格局β的状态)。由于DPN M所有可达格局都是弱相关，即可达格局β为弱相关格局，因此至少存在一个对应的强相关格局β′＝<p，R′>。由定律1可知在迁移系统M的一个正则格局β，存在一个强相关格局β′和转换成R′的集合S，在T里必定存在与之对应格局γ，存在γ|＝_Sβ并且即状态p_F(p_F为格局γ的状态)在T可达。

再证必要性：状态p_F在TDPN可达其转换状态p_F′在DPN可达。

如果目标状态p_F′在T是可达，由定理1可知在M里必定存在与之对于格局β(p_F′为格局β的状态)，因此至少存在一个强相关格局β′＝<p，R′>。由定律2可知在迁移系统T的一个格局γ，存在一个强相关格局β′和转换成R′的域集合S，在M里必定存在与之对应格局β，存在γ|＝_Sβ并且即状态p_F′(p_F′为格局β的状态)在M可达。

因此，状态p_F在TDPN可达当且仅当其转换状态p_F′在DPN可达。

通过以上方法步骤可以查找出并发递归程序中存在的设计错误或漏洞，保证程序的可靠性与正确性。本方法为自动化的可达性求解方法，可以实现时间动态下推网络可达性问题的可判定求解，而无需用户过多参与，可达格局计算过程简单、有效。

Claims (1)

1.时间动态下推网络的转换方法，其特征是，包括如下步骤：

步骤(1)把实时并发递归程序转换为一个时间动态下推网络；

步骤(1.1)构造实时并发递归程序的抽象模型即时间动态下推网络；

所构造的时间动态下推网络是一个四元组T＝(P，Γ，Δ，X)，其中P是状态集；Γ是栈字符集；Δ＝Δ_nop∪Δ＝∪Δ_├∪Δ_push∪Δ_pop∪Δ_dc是迁移规则集合，其中Δ_nop表示空操作迁移，Δ＝表示时钟赋值迁移，Δ_├表示时间流逝迁移，Δ_push表示入栈迁移，Δ_pop表示出栈迁移，Δ_dc表示动态线程创建迁移；X表示时钟集，其取值函数表示对于在当前取值为θ(x)；

所构造时间动态下推网络格局表示所述模型在某一时刻的状态，其中：表示当前全局变量g和其年龄θ(g)的二元组<g,θ(g)>；p_i∈P表示局部状态节点，表示栈序列为i的栈内容ω_i和其年龄θ(ω_i)的二元组<ω_i,θ(ω_i)>；表示时钟x和其取值θ(x)的二元组<x,θ(x)>；

步骤(1.2)将所构造的时间动态下推网络用操作语义进行描述；

时间动态下推网络作为实时多线程程序的模型，用于描述多个下推系统同时产生迁移，其迁移关系Δ＝Δ_nop∪Δ＝∪Δ_├∪Δ_push∪Δ_pop∪Δ_dc下面根据不同的迁移动作op给出其执行含义；

1)Δ＝Δ_nop时，op＝nop，表示格局内元素未发生变化；

2)Δ＝Δ＝时，op＝x←I，v∈I；表示给时钟x指定I范围内的任意值v，其它格局内元素未发生变化；

3)Δ＝Δ_├时，op＝Time←c，假设那么表示格局内所有时钟增加v，格局内非时钟内容未发生变化；

4)Δ＝Δ_push时，op＝push(a,I)，v∈I，表示将变量a压入栈顶，并设定相应时钟为x，其时钟值为I范围内的任意值；

5)Δ＝Δ_pop时，op＝pop(a,I)，v∈I，表示将栈顶内时钟值为I范围的变量a弹出；

6)Δ＝Δ_dc时，表示创建新线程dc的栈内容

步骤(2)将步骤(1)所获得的时间动态下推网络T＝(P,Γ,Δ,X)，通过下述转换方法转换为动态下推网络M＝(P^M,Γ^M,Δ^M)；

步骤(2.1)状态P^M的转换：即T的状态集与M的状态集相同；

步骤(2.2)栈字符集的转换：若a∈{Γ,├},则且其中a^·表示记录栈字符a的时间流逝，符号表示向下取整；

步骤(2.3)迁移关系Δ到Δ^M的转换规则；

设该下推系统的栈深度为l，且栈底编号为1，栈顶编号为l；时间动态下推网络即TDPN含有全局变量g，时钟变量x，栈内容ω＝{ω₁…ω_i…ω_n}，其中ω_i表示i号下推系统的栈内容，用ω_il|Γ表示ω_i投影在Γ的栈顶字符；各表示其年龄和取值在时钟等价下的关键点；从而可知对应在M的当前时钟等价域 其中表示域R_l记录栈顶字符，├表示域R_l的参考时钟字符，├^·表示域R_l对应的时间流逝字符；

TDPN格局φ＝(γ,op,γ′)∈Δ表示T的格局迁移，对应M的格局迁移可表示为其中p和p′与T中状态相同，分别表示格局迁移前后的状态；R_l＝{R_1l…R_il…R_nl}表示栈顶域，其中R_il表示i号下推系统的栈顶域，R_l和R_l′分别表示格局迁移前后的栈顶域；动作迁移集op′对应于T的op，下面描述根据不同的op构造R_l′：

1)当op＝nop时，对于当且仅当M中存在 在T中空操作只改变了状态，所以在M中格局迁移也只改变状态，域R_l保持不变；

2)当op＝(x←I)时，对于当且仅当M中存在 该迁移关系表示对DPN域R_l中时钟为x的项执行操作，其中θ(x)′∈I，来构造域R_l′；具体执行过程如下：

域R_l出栈，获得R_l里的项重置θ(x)为θ(x)′，形成新项

项代替域R_l中的项获得域R_l′，并入栈，转换到新的状态p′；

3)当op＝(Time←v)时，对于当且仅当M中存在该迁移关系表示域R_l中除了参考时钟项(├，0)，其余所有项的时钟值加上时间流逝v，来构造域R_l ⁺；具体执行步骤为：

域R_l出栈，除了参考时钟，全部加上时间流逝v， 表示对应于g、ω_il、x的新普通项，各表示相应的新记录项，表示参考时钟记录项；

新项代替原来项，得到域R_l ⁺，并入栈，转换到新的状态p′；

4)当op＝push(a,I)时，对于当且仅当M存在该迁移关系表示，对i号下推系统进行入栈操作，将字符为a，值为的项入栈域R_il，来构造域R_i(l+1)；具体过程如下：

从R_il获得项和

分别代替 获得域R_i(l+1)，并入栈，转换到新的状态p′；

5)当op＝pop(a,I)时，对于当且仅当M存在 该迁移关系表示，出栈域R_il中栈字符为a，且θ(a)∈I的项，来构造域R_il′；具体步骤描述如下：

出栈域R_il和域R_i(l-1)，获得域R_il里的项

域R_(l-1)中所有项的时钟值加上θ(├^·)，获得域R_i(l-1)′；

通过R_il和R_i(l-1)′获得域R_il′，R_il′项分别为：普通栈字符项来自域R_i(l-1)′；普通时钟项、全局变量项来自域R_il；记录项全部来自域R_i(l-1)′；

入栈域R_il′，转换到新的状态p′；

6)当op＝dc时，对于当且仅当M中存在 该迁移关系表示，创建新线程来构造域R_l′；假设TDPN模型，动态创建新下推系统的栈编号为n+1；具体执行步骤如下：

出栈域R_l，基于关键点的时钟等价优化技术，可得普通字符项记录项

把项和加入域R_l，得到域R_l′，并入栈，转换到新的状态p′。