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

摘要

本发明公开一种时间多栈下推网络的动态转换方法，首先，在MPDN的基础上引入时钟，提出TMPDN模型，并给出其语法及操作语义；其次，利用时钟域等价的优化技术，通过动态转换方法，将连续时间的TMPDN模型转换成离散的多栈下推网络模型。本发明能够实现同时实现实时并发系统的实时性和并发性的描述，并能为实时并发程序的形式化验证提供保证。

主权项

时间多栈下推网络的动态转换方法，其特征是，包括如下步骤：步骤(1)将含有时间行为的并发递归程序转换为一个等价的可模拟程序执行的时间多栈下推网络，该时间多栈下推网络的执行对应于程序包含的所有动作或行为；步骤(1.1)构造实时并发递归程序的抽象模型即时间多栈下推网络；所构造的时间多栈下推网络是一个六元组M_T＝(n,Q,q₀,Γ,T,Δ)；其中n表示系统中栈的个数；Q表示有限状态集；q₀表示初始状态；Γ表示有限栈符集；T＝T_G∪T_L表示有限时钟集，T_G表示全局时钟，用于标识实时并发系统中全局变量或事务的时间，T_L表示栈内局部时钟，用于标识系统中局部变量或子事务的时间；迁移关系$\Delta \subseteq 2^{\left[n\right]}\times Q\times T_G\times {(\Gamma \times T_L)}^{*}\times 2^{\left[n\right]}\times Q\times T_G\times$${(\Gamma \times T_L)}^{*}$为描述系统格局的迁移；所构造的时间多栈下推网络的格局C＝<Work[n],q,{w_i}_i∈[n],v>；其中q∈Q，为[n]子集，表示当前工作栈集，w_i为栈i的字，表示栈i的内容，描述为w_i∈(Γ×⁺)^*，v表示时钟当前取值；步骤(1.2)将所构造的时间多栈下推网络用操作语义进行描述，其中时间多栈下推网络作为实时并发程序的模型，用于描述多个栈同时产生迁移，其迁移关系Δ分为栈内迁移Δⁱⁿ、栈间切换Δ^inter和并发执行Δ^||；步骤(1.2.1)对于一个栈i内迁移的执行，用形式表示，其中op_in为栈内迁移时的动作集，包括空操作nop、时间约束判断t∈I？、时钟重置t←I、时间流逝Time←c、压栈操作push(a,I)和出栈操作pop(a,I)，其中I表示时钟取值范围，t∈T，Time表示具体时钟值，故栈内迁移关系Δⁱⁿ表示为Δ^nop∪Δ^？∪Δ^＝∪Δ^├∪Δ^push∪Δ^pop，其中Δ^nop、Δ^？、Δ^＝、Δ^├、Δ^push和Δ^pop分别表示上述操作的迁移；根据不同的栈内迁移动作op_in给出具体的操作含义如下：1)Δⁱⁿ＝Δ^nop：op_in＝nop，w_i′＝w_i，v′＝v；表示格局内元素未发生变化；2)Δⁱⁿ＝Δ^？：op_in＝t∈I？，w_i′＝w_i，v′＝v，v(t)∈I；表示当t的时钟值在I范围内时，执行该操作，格局内元素未发生变化；3)Δⁱⁿ＝Δ^＝：op_in＝t←I，w_i′＝w_i，v′＝v[t←c]，c∈I；表示给时钟t指定I范围内的任意值c，其它格局内元素未发生变化；4)Δⁱⁿ＝Δ^├：op_in＝Time←c，w_i′＝w_i^+c，假设w_i＝<a₁,v₁><a₂,v₂>…<a_n,v_n>，那么w_i^+c＝<a₁,v₁+c><a₂,v₂+c>…<a_n,v_n+c>，v′＝v+c；表示格局内所有时钟增加c，格局内非时钟内容未发生变化；5)Δⁱⁿ＝Δ^push：op_in＝push(a,I),w_i′＝w_i·<a,c>，c∈I，v′＝v；表示将变量a压入栈顶，并设定相应时钟为t，其时钟值为I范围内的任意值；6)Δⁱⁿ＝Δ^pop：op_in＝pop(a,I)，w_i＝w_i′·<a,c>，c∈I，v′＝v；表示将栈顶内时钟值为I范围的变量a弹出；步骤(1.2.2)描述栈间切换Δ^inter；假设栈间切换操作op_inter＝i＞j表示栈i切换到栈j，用形式表示，其中q和q′∈Q；v′＝v；w_i,w_j分别为栈i和j的字，i和j∈[n]且i≠j；上下文切换时，将栈j从等待栈切换到工作栈，同时将栈i从工作栈切换到等待栈，则切换后的工作栈Work[n]′＝Work[n]/{i}∪{j}；步骤(1.2.3)描述并发操作Δ^||；假设op＝op_in∪op_inter为栈迁移动作集，并发执行用形式表示，Work[n]为当前工作栈集，如果不发生栈间切换，则Work[n]′＝Work[n]，如果发生栈间切换i＞j，则Work[n]′＝Work[n]/{i}∪{j}；步骤(2)将步骤(1)所给定的一个时间多栈下推网络M_T＝([n],Q,q₀,Γ,T,Δ)，通过下述动态转换过程获得多栈下推网络M_M＝([n]^M,Q^M,q₀^M,Γ^M,Δ^M)：1)栈个数[n]^M的转换：[n]^M＝[n]，即M_M的栈数量与M_T的栈数量相等；2)状态Q^M的转换：Q^M＝Q，即M_T的状态集与M_M的状态集相同；3)初始状态q₀^M的转换：q₀^M＝q₀，即M_M的初始状态与M_T的初始状态相同；4)栈字符Γ^M的转换：Γ^M＝2^Z×key，其中Z:＝Y∪Y^·，增加了标识项以及基础时间字符，key为时钟关键点集；5)迁移关系Δ^M的转换规则：M_T的格局迁移为w_i∈(Γ×⁺)^*为栈i的字，设d_i为栈i的栈深度，用w_ij表示栈i内第j层的子字，为栈i的栈顶子字，j∈[d_i]，w_ij|_Γ表示w_ij投影在Γ的栈字符，v(w_ij|_Γ)表示投影与栈字符Γ相关联的时钟值，表示投影与栈字符Γ相关联的时钟值在时钟等价后的关键点，T_G为全局时钟，表示全局时钟的时钟值在时钟域等价后的关键点；下面具体描述不同op的构造：5.1)Δ＝Δ^nop时，op＝nop，如果那么在M_M中有与之对应，即两者nop操作相同；5.2)Δ＝Δ^？时，op＝t∈I？，在M_M中有迁移关系Δ^M？与Δ^？相对应；此时M_M的格局进行迁移首先将栈顶域出栈，转入状态对字符t的关键点进行判断后，再将入栈，状态为最终状态q′，整个过程中栈内字符并未改变；5.3)Δ＝Δ^＝时，op＝t←I，在M_M中有迁移关系Δ^M＝与Δ^＝相对应；此时M_M的格局进行迁移其中迁移关系Δ^M＝表示对{R_i1}进行赋值操作，v(t)∈I为M_T赋值时钟值，首先栈顶域出栈，转入状态给内任意栈内字符或者全局时钟t，赋予I中任意一个值对应的关键点之后再将赋值后的入栈，获得状态q′；5.4)Δ＝Δ^├时，op＝Time←c，在M_M中有迁移关系Δ^M├与Δ^├相对应；此时M_M的格局进行迁移首先栈顶域出栈，得状态之后将项内非基础时间字符t的时钟值，增加时钟值c后取关键点，并将关键点赋予字符t，再将赋值后的入栈，最后获得状态q′；5.5)Δ＝Δ^pop时，op＝pop(a,I)，在M_M中有迁移关系Δ^Mpop与Δ^pop相对应；此时M_M的格局进行迁移其中为和的组合域，首先栈顶域出栈，得状态然后将下一层域出栈，转入状态最后将和的组合域入栈，转入状态q′；5.6)Δ＝Δ^push时，op＝push(a,I)，在M_M中有迁移关系Δ^Mpush与Δ^push相首先将栈顶域出栈，然后再将域入栈，最后将含字符a的域入栈；5.7)Δ＝Δ^inter时，在M_M中有迁移关系Δ^Minter与Δ^inter相对应；此时M_M的格局进行迁移其中{R_i}和{R_j}分别为栈i和j的域，i和j∈[n]且i≠j；上下文切换时，将栈j从等待栈切换到工作栈，同时将栈i从工作栈切换到等待栈；5.8)Δ＝Δ^||时，在M_M中有迁移关系Δ^M||与Δ^||相对应；此时M_M的格局进行迁移工作栈集Work[n]内的每个栈，调用相应的栈内迁移转换，转换后格局为<Work[n]′,q′,{R_j}_j∈[n]>。