基于上下文定界的队列通信并发递归程序验证方法

摘要

基于上下文定界的消息队列通信并发递归程序的验证方法属于软件安全、可靠性技术领域，其特征在于通过对每个下推系统迭代地应用Post*算法，穷尽搜索其执行的状态空间，并通过有限的上下文切换次数k利用上下文切换函数实现不同上下文间的切换，以模拟各个进程之间的交错执行，得到k次上下文执行内的可达格局集合，通过计算可达格局集合与目标格局集合的交集是否为空，判断出目标格局集合即状态是否可达，从而确定程序中存在的设计错误或漏洞，保证程序的正确与可靠。本发明无需用户过多参与，实现了基于可达性求解的程序自动化检验，而且格局计算过程简单而有效，在良序排队约束的条件下，本发明提出的上下文定界可达性是可以判定的。

主权项

1.基于上下文定界的消息队列通信并发递归程序的验证方法，其特征在于：是一种基于良序消息队列通信的并发递归程序RQCP上下文切换定界的可达性辨识之上的程序验证方法，所述良序消息队里是仅当进程的局部栈为空时，进程才能从队列中读取消息中途不允许被中断，直至执行结束时才处理下一个任务，所述的并发递归程序，以下简称RQCP，用R表示，是在一台多核处理器中依次按以下步骤实现验证的，步骤（1）、依次按以下步骤把所述的R转换为一个多栈下推系统，用表示，以便把上下文(p,q)切换定界可达性问题转换为多栈下推系统的阶定界可达性问题，其中k次上下文切换对应于3k+1个阶，其目的在于把基于良序消息队列通信的并发递归程序R转换为一个等价的用于模拟R执行的多栈下推系统，该多栈下推系统的执行对应于所述R所包含的动作或行为，步骤如下：步骤（1.1）、构建R的抽象模型给定一个体系结构A=(P,Q,Sender,Receiver)，P是有限进程集合，Q是有限队列集合，Sender:Q→P和Receiver:Q→P是两个指派函数，分别为每个队列q∈Q唯一指派的发送进程和接收进程，并规定每个队列的发送进程和接收进程是不同的：即对于q∈Q，Sender(q)≠Receiver(q)，设：Π表示有限的消息字母表，m∈Π表示消息，p∈P表示一个进程，q∈Q表示一个队列；Act_p表示一个进程p的动作集合，Act=∪_p∈PAct_p表示所有进程的动作集合；Calls表示所有进程的调用动作的集合，表述为{p:call|p∈P}，p:call为描述过程调用的局部栈动作；Rets表示所有进程的返回动作的集合，表述为{p:ret|p∈P}，p:ret为描述过程返回的局部栈动作；其中：p:call相当于进程p的局部过程调用，进程p把至少包括地址、局部变量的赋值在内的数据送到局部栈的栈顶，并迁移到新状态；p:ret相当于进程p中过程调用的返回，弹出局部栈的内容并迁移到另一个新状态，所述另一个新状态依赖于进程p的当前状态及所述的局部栈中弹出的数据；动作p:send(q,m)表示进程p向接收队列q中写入消息m；动作p:recv(q,m)表示进程p从所述接收队列q中读取消息m；动作p:int表示进程p的对队列不处理的一个内部动作；给定一个体系结构A=(P,Q,Sender,Receiver)，在所述体系结构A运行的上的递归队列并发程序是一个五元组R，R=(S,s₀,∏，Γ，{T_p}_p∈P)，其中S是有限的状态集合，s₀∈S是初始状态，Π是所述的有限的消息字母表，Γ是有限的局部栈字母表，T_p是进程p的迁移关系集合，表示如下：$T_p\subseteq (S\times ({\mathrm{Act}}_p/\{p:\mathrm{call},p:\mathrm{ret}\left\}\right)\times S)\cup (S\times \{p:\mathrm{call}\}\times S\times \Gamma )\cup (S\times \{p:\mathrm{ret})\times \Gamma \times S),$其中进程p的动作的形式如下：1)p:send(q,m)，其中m∈Π，q∈Q，且Sender(q)=p；2)p:recv(q,m)，其中m∈Π，q∈Q，且Receiver(q)=p；3)p:int，或者p:call或者p:ret；步骤（1.2）、R的操作语义描述给定递归队列并发程序R=(S,s₀,∏，Γ，{T_p}_p∈P)，其中：{T_p}_p∈P是所有进程p的迁移关系集合；其格局是一个三元组(s,{σ_p}_p∈P,{μ_q}_q∈Q)，其中s∈S是状态；符号{σ_p}∈Γ^*是进程p的进程局部栈的内容，表示为σ_p∈Γ^*，Γ^*是所述进程局部栈字母上的闭包；符号{μ_q}∈Π^*是队列q的内容，表示为μ_q∈Π^*，Π^*是所述消息字母上的闭包；假设进程p的栈顶内容位于σ_p的最左端，栈底内容位于σ_p的最右端；队列q的队尾消息位于μ_q的最左端，队头消息位于μ_q的最右端；使用以下操作语义描述格局之间的迁移关系：操作$\left[\mathrm{Internal}\right]\frac{\begin{array}{cc}\mathrm{act}=p:\mathrm{int}& (s,p:\mathrm{int},s^{\prime })\in T_p\end{array}}{(s,{\left\{{\sigma }_p\right\}}_{p\in P},{\left\{{\mu }_q\right\}}_{q\in Q})\stackrel{\mathrm{sct}}{\to }(s^{\prime },{\left\{{\sigma }_p\right\}}_{p\in P},{\left\{{\mu }_q\right\}}_{q\in Q})}$为内部动作，表示：执行动作p:int，使R的状态由但{σ_p}、{μ_q}的内容没有改变；操作$\left[\mathrm{Send}\right]\frac{\begin{array}{ccc}\mathrm{act}=p:\mathrm{send}(q,m)& (s,p:\mathrm{send}(q,m),s^{\prime })\in T_p& \mathrm{Sender}\left(q\right)=p\end{array}}{(s,{\left\{{\sigma }_p\right\}}_{p\in P},{\left\{{\mu }_{q^{\prime }}\right\}}_{q^{\prime }\in (Q/\{q\left\}\right)}\cup \{{\mu }_q\left\}\right)\stackrel{\mathrm{act}}{\to }(s^{\prime },{\left\{{\sigma }_p\right\}}_{p\in P},{\left\{{\mu }_{q^{\prime }}\right\}}_{q^{\prime }\in (Q/\{q\left\}\right)}\cup \{m.{\mu }_q\left\}\right)}$为写入，表示：执行动作p:send(q,m)，写入进程为p，使R的状态由使队列的内容{μ_q′}中除了{μ_q}外还写入了消息m；操作$\left[\mathrm{Receive}\right]\frac{\begin{array}{ccc}\mathrm{act}=p:\mathrm{recv}(q,m)& (s,p:\mathrm{recv}(q,m),s^{\prime })\in T_p& \mathrm{Receiver}\left(q\right)=p\end{array}}{(s,{\left\{{\sigma }_p\right\}}_{p\in P},{\left\{{\mu }_{q^{\prime }}\right\}}_{q^{\prime }\in (Q/\{q\left\}\right)}\cup \{{\mu }_q^{\prime }.m\left\}\right)\stackrel{\mathrm{act}}{\to }(s^{\prime },{\left\{{\sigma }_p\right\}}_{p\in P},{\left\{{\mu }_{q^{\prime }}\right\}}_{q^{\prime }\in (Q/\{q\left\}\right)}\cup \{{\mu }_q^{\prime }\left\}\right)}$为接受，表示执行动作p:recv(q,m)，读取方是p，从s状态下的队列{μ′_q.m}中读取消息m，使R的状态由使队列q的内容{μ′_q}中被读取了消息m，写入时的{μ_q}不一定等于读取时的{μ′_q}；操作$\left[\mathrm{Call}\right]\frac{\begin{array}{cc}\mathrm{act}=p:\mathrm{call}& (s,p:\mathrm{call},s^{\prime },\gamma )\in T_p\end{array}}{(s,\{{\sigma }_p\}\cup {\left\{{\sigma }_{p^{\prime }}\right\}}_{p^{\prime }\in (P/\{p\left\}\right)},{\left\{{\mu }_q\right\}}_{q\in Q})\stackrel{\mathrm{act}}{\to }(s^{\prime },\{\gamma {\sigma }_p\}\cup {\left\{{\sigma }_{p^{\prime }}\right\}}_{p^{\prime }\in (P/\{p\left\}\right)},{\left\{{\mu }_q\right\}}_{q\in Q})}$为调用，表示：执行动作p:call，在s状态下进程p根据规则γ调用至少包括地址、局部变量的赋值在内的数据送到对应于进程p的局部栈的内容{σ_p′}的最左端，使得状态由{σ_p′}添加为{γσ_p′}；操作$\left[\mathrm{Return}\right]\frac{\begin{array}{cc}\mathrm{act}=p:\mathrm{ret}& (s,p:\mathrm{ret},\gamma ,s^{\prime })\in T_p\end{array}}{(s,\{{{\mathrm{\gamma \sigma }}^{\prime }}_p\}\cup {\left\{{\sigma }_{p^{\prime }}\right\}}_{p^{\prime }\in (P/\{p\left\}\right)},{\left\{{\mu }_q\right\}}_{q\in Q})\stackrel{\mathrm{act}}{\to }(s^{\prime },\{{{\sigma }^{\prime }}_p\}\cup {\left\{{\sigma }_{p^{\prime }}\right\}}_{p^{\prime }\in (P/\{p\left\}\right)},{\left\{{\mu }_q\right\}}_{q\in Q})}$为返回，表示：执行动作p:ret，在s状态下，根据规则γ，弹出进程p的进程局部栈的内容{γσ′_p}中按规则γ调用的至少包括地址、局部变量的赋值在内的数据，剩下原先的内容{σ′_p}，使状态状态，所述调用的{γσ′_p}与返回的{σ′_p}不一定相同；步骤（1.3）、用一个多栈下推系统模拟良序消息队列的并发递归程序的执行给定：良序消息队列的并发递归程序R=(S,s₀,∏，Γ，{T_p}_p∈P)，构造一个模拟所述良序消息队列的并发递归程序R的k-上下文切换定界执行的多栈下推系统其中：S是有限的状态集合，s₀∈S是初始状态；St是局部栈集合，包括工作局部栈st_w，进程p对应的局部栈st_p，队列q∈Q对应的局部栈st_q，St表示为St={st_w∪{st_p}_p∈P∪{st_q}_q∈Q}，各局部栈初始化为空；是字母表，包括队列对应的局部栈字母表，与进程对应的局部栈的字母表，表示为Δ是迁移关系集合，包括：Δ_int内部迁移关系集合，Δ_push写入迁移关系集合，包括push_q和push_p，其中：push_q与进程p的写入队列操作相关的迁移关系，push_p与进程p的入栈操作相关的迁移关系，Δ_pop读取迁移关系集合，包括pop_q和pop_p，其中：pop_q与进程p的读取队列操作相关的迁移关系，pop_p与进程p的出栈操作相关的迁移关系，从而得到迁移关系集合Δ的表达式为：Δ=Δ_int∪Δ_pop∪Δ_push，在上下文（p,q）内，所述上下文定义为：某个进程任意长度的连续执行序列，进程p仅能从一个队列中读取消息，但可向所有输出消息的任一队列q写入消息，所述进程p能执行的迁移关系定义如下：规则$\left[\mathrm{internal}\right]\frac{(s,p:\mathrm{int},s^{\prime })\in T_p}{(s,p:\mathrm{int},s^{\prime })\in {\Delta }_{\mathrm{int}}},$规则$\left[{\mathrm{push}}_q\right]\frac{\begin{array}{cc}(s,p:\mathrm{send}(q,m),s^{\prime })\in T_p& \mathrm{Sender}\left(q\right)=p\end{array}}{(s,p:\mathrm{send}(q,m),s^{\prime })\in {\Delta }_{\mathrm{push}}},$规则$\left[{\mathrm{push}}_p\right]\frac{(s,p:\mathrm{call},s^{\prime },\gamma )\in T_p}{(s,p:\mathrm{call},s^{\prime },\gamma )\in {\Delta }_{\mathrm{push}}},$规则$\left[{\mathrm{pop}}_q\right]\frac{\begin{array}{cc}(s,p:\mathrm{recv}(p,m),s^{\prime })\in T_p& \mathrm{Receiver}\left(q\right)=p\end{array}}{(s,p:\mathrm{recv}(q,m),s^{\prime })\in {\Delta }_{\mathrm{pop}}},$规则$\left[{\mathrm{pop}}_p\right]\frac{(s,p:\mathrm{ret},\gamma ,s^{\prime })\in T_p}{(s,p:\mathrm{ret},\gamma ,s^{\prime })\in {\Delta }_{\mathrm{pop}}},$规则表示把所述的R内队列操作相关的迁移关系添加到所述的多栈下推系统中对应的迁移关系集合中去，根据以上转换方法构造的多栈下推系统能模拟良序排队的递归队列并发程序R的执行，并且的3k+1阶定界可达问题相当于R的k上下文切换定界可达问题；步骤（2）、按如下步骤执行基于可达算法Post^*的可达格局集合Reach计算步骤（2.1）、初始化多栈下推系统设立多栈下推系统和上下文切换次数K，0≤k≤K，其中：多栈下推系统是下推系统的自然扩展，包含多个栈结构；K是一个正整数，也是Post^*算法的迭代次数；其中：S是有限的状态集合，s₀∈S是初始状态；St={st_w∪{st_p}_p∈P∪{st_q}_q∈Q}，初始时，各栈st∈St的栈内容σ_st为空，表示为σ_st=ε；其中：Π是队列对应的局部栈字母表，Γ是进程对应的局部栈的字母表，总称字母表；Δ是迁移关系集合，Δ=Δ_int∪Δ_pop∪Δ_push；定义：输出可达格局集合Reach，集合Reach中存储的是在至多k次上下文切换执行内正向可达的格局，用c表示，c=<s₀,{σ_st}_st∈St>，σ_st表示栈st∈St的内容；多栈下推系统的初始格局是c_in=<s₀,{σ_st}_st∈St>，以及对应的切换次数k，以格局项(c,k)的形式存储在所述可达格局Reach的工作列表WL上，初始时的初始格局是c_in=<s₀,{σ_st}_st∈St>，内容σ_st为空，给定的目标格局状态集合T，所述目标状态集合T定义为一种错误状态集合，表示为是一种在所述并发递归程序不可能出现的错误状态的集合，步骤（2.2）、建立工作列表WL按照所述并发递归程序的执行顺序把所述上下文(p,q)转换为依次衔接的格局项(c,k)，0≤k≤K的编号存储于工作列表内，并初始化所述初始格为c_in，步骤（2.3）、初始上下文(p,q)选择定义二元组（p,q）是所述并发递归程序的一个执行上下文，其中p是进程，q是进程间通信的队列，并且随机或指定某个上下文（p,q）为初始上下文，并对各栈st初始化：根据队列q和进程p对应的迁移关系集合Δ，把队列q对应栈st_q的内容压入工作栈st_w的底部，将进程p对应的栈st_p内容压入工作栈st_w的顶部，假定是上下文（p,q）下进程p的下推系统，建立接受上下文(p,q)的初始格局的下推自动机A_p=(Q,Г，→₀,P,F)，对应算法5中的自动机A，其中：Q是自动机的控制位置集合，对应算法5中自动机A的状态集合；Γ是自动机接受的字母表，对应算法5中自动机A接受的字母表；→₀是自动机的转移函数，P是初始控制位置集合，对应算法5中自动机A的初始状态集合；F是终止控制位置集合，对应算法5中自动机A的终止状态集合，对于下推自动机A_p，存在接受其正向可达格局集合的下推自动机A′_p=post^*(A_p)，给定初始格局为<s₀,σ_st>的下推系统及其对应的迁移关系集合Δ，可以计算接受下推系统正向可达格局集合为语言的下推自动机步骤（2.4）、按以下步骤从所述初始上下文(p,q)开始，对所述工作队列表WL中各个格局项编号中的内容进行上下文切换可达性计算步骤（2.4.1）、从工作列表WL中取出一个编号对应于初始上下文(p,q)的格局项，并分别存储在进程局部栈st_p和队列局部栈st_q中：进程p逆序地存储存储在st_p和中，栈底存储队尾指向的内容，栈顶存储队头指向的内容，队列q是顺序存储在栈st_q中：栈顶存储队尾指向的内容，栈底存储队头指向的内容，步骤（2.4.2）、再把栈st_q的内容存储在工作栈st_w的底部，栈st_p的内容存储在工作栈st_w的顶部，步骤（2.4.3）、使另一个进程局部栈栈st_p和队列栈st_q初始化为空，在把初始上下文(p,q)切换为上下文(p′,q′)时，此时迭代次数k≤K,对工作栈st_w的顶部和底部进行出栈操作，把读取的内容分别存储到栈st_p和st_q中，步骤（2.4.4）、按以下步骤计算进程中的初始格局是否属于正向可达格局集合的初始格局：步骤（2.4.4.1）、若所述多栈下推系统中对应于初始上下文(p,q)的迁移关系集合是写入迁移关系集合Δ_push，δ=(s,st_q′,a,s′)∈Δ_push，a是消息，且格局<s ′σ′_p>，σ′_p=aσ_p，σ_p是栈st_p的内容，则向栈st_q′中入栈消息a，步骤（2.4.4.2）、若所述多栈下推系统中对应于初始上下文(p,q)的迁移关系集合是读取迁移关系集合Δ_pop，δ=(s,st_q,a,s′)，且格局为<s′,ε>，则弹出栈st_q内的消息a，局部栈为空，步骤（2.4.4.3）、修改状态s′的可达格局赋值为x，把格局项(x,i+1)添加到工作列表WL中，步骤（2.4.4.4）、在继续从初始上下文(p,q)开始向下执行上下文切换之后，按步骤（2.5）所述进行可达格局集合Reach计算，步骤（2.5）、根据Post^*算法计算接受上下文（p,q）正向可达格局集合的下推自动机A′_p=Post^*(A_p)，A_p是接受进程p初始格局的下推自动机，修改A′_p的状态，修改后的格局添加到工作列表WL，以及可达格局集合Reach，步骤（2.5.1）、对于s′∈S(A′_p)，如果下推自动机A_p∈{P/p}的初始状态与状态s相同，使用rename(A_p∈{P/p},s′)修改A_p∈{P/p}的初始状态为s′，避免自动机A′_p的初始状态与自动机A_p中的状态重名而产生冲突，步骤（2.5.2）、使用函数update(A′_p,s′)重命名A′_p中除s′之外的其他状态，并更新S不包含的状态，即修改格局的赋值为x=<s′,update(A′_p,s′),rename(A_p∈{P/p},s′),update(σ_st/{p∈P})>，步骤（2.5.3）、最后修改后的可达格局赋值为x，将格局项(x,k+1)添加到工作列表WL，并将格局x添加到集合Reach，步骤（3）、目标可达性的判定分析根据正向可达格局集合Reach(k)和给定的目标状态集合T，目标状态集合T视为R中不可能出现的状态的集合，也称错误状态集合，进而计算集合Reach和集合的交集是否为空，上下文切换次数k的值从0不断增大，直至可用计算资源被耗尽，步骤（3.1）、若Reach∩T非空，则经过k次上下文切换的运行，某个目标状态s∈S是可达的，则存在一个起始于初始格局的执行路径能够到达该错误状态，进而根据进程在各个状态的局部栈的内容和消息队列的内容，尝试查找产生错误的原因，步骤（3.2）、若Reach∩T为空，则经过k次上下文切换的运行，目标状态s∈S是不可达的，状态s不可达的判断步骤如下：a)经过k次上下文切换的运行，搜索的状态空间覆盖度不足以覆盖目标状态，此时可以增大k的值并继续求解，直至耗尽所有可用的计算资源；b)若根据步骤a)仍不能判定目标状态是可达的，则得出结论：在现有计算能力下目标状态是不可能出现的。