基于SAT的命题投影时序逻辑限界模型检测方法

摘要

本发明是一种基于SAT的命题投影时序逻辑限界模型检测方法，步骤是：用Kripke结构描述待验证系统模型M；用PPTL公式描述性质P；设定限界k；将PPTL限界模型检测转换为SAT问题；对SAT问题求解：有解，系统M不满足性质P，给出反例，无解，系统M有界满足性质P，增大k值，进入下一个检测周期，直到k值足够大且在每个限界模型检测周期内待验证系统M都有界满足性质P。本发明使用PPTL描述系统性质，解决了CTL和LTL表达能力有限的问题，并通过限制搜索长度减少搜索状态数，缓解了状态空间爆炸，融合了PPTL和BMC各自的优点，使系统复杂性质的验证更方便有效。本发明适用于软硬件系统以及通信协议的形式化验证。

主权项

一种用于通信系统和调度系统的基于SAT的命题投影时序逻辑限界模型检测方法，其特征在于：具体检测步骤包括：步骤1.首先为待验证系统建立模型M，M是一个描述待验证系统行为的有限状态迁移系统，采用Kripke结构描述模型M；步骤2.使用命题投影时序逻辑PPTL公式描述待验证系统的性质，得到PPTL描述的性质公式P，并将其等价转换为正则形NF，得到性质公式P的正则形NF(P)，进而得到性质非的正则形步骤3.设定限界模型检测的界限k，k为一个不大于完整区间长度的正整数，用来限定进行限界模型检测时的搜索长度，界限k的值在一个限界模型检测周期内是不变的，在下一个限界模型检测周期内可根据当前周期的检测结果进行调整；步骤4.根据PPTL限界模型检测向命题可满足性问题SAT转换的转换规则，结合设定的限界模型检测界限k，对待验证系统模型M和性质的非进行编码，通过布尔编码将限界模型检测问题转化为命题可满足性SAT问题；具体步骤包括：步骤4.1.根据待验证系统Kripke结构模型M的标记函数L，用布尔向量表示待验证系统中的状态和迁移关系，完成待验证系统约束条件的编码过程，约束条件其中k为界限，I(s₀)表示状态s₀是初始状态，T(s_i，s_i+1)表示从状态s_i到状态s_i+1的状态迁移关系，表示状态序列(s₀，s₁，...，s_k)中从状态s₀经过状态s₁，s₂，...，s_i，...，s_k‑1到达状态s_k的一系列状态迁移，若状态序列(s₀，s₁，...，s_k)是从初始状态出发的有效区间，则存在一组赋值使得约束条件M_k为真；步骤4.2.在界限k下，将待验证系统性质P转换为等价的命题公式：待验证系统的性质P的约束条件L_k是在界限k下区间的循环条件，根据搜索区间的结构，确定区间结构相关部分L_k的真假值，区间为有循环的无穷区间时，L_k为真，区间为无循环的有穷区间时，L_k为假；根据限界模型检测过程中PPTL性质公式P向命题公式的等价转换规则对性质约束条件中性质相关部分和进行等价转换，进而得到约束条件X_k等价的命题公式，其中0为初始状态s₀下标，k为界限，l为状态s_l下标，是无循环有穷区间下的性质约束条件，记录了所有可能的从状态s_k到之前状态的迁移，L_(k，l)表示存在从状态s_k到向前状态s_l(l∈N，0≤l≤k)的状态迁移，循环的状态序列段为(s_l，...，s_k)，表示在界限k内，该区间是无循环有穷的区间，是无循环有穷区间在界限k下的性质相关部分；是有循环无穷区间下的性质约束条件，是有循环无穷区间在界限k下的性质相关部分，表示所有可能的循环及其相应的性质约束；针对搜索区间的不同结构，给出限界模型检测过程中PPTL逻辑公式向命题公式转换的不同的等价转换规则，即PPTL限界模型检测向命题可满足性问题SAT转换的转换规则，已知搜索区间分为两种：有循环的无穷区间和无循环的有穷区间，根据搜索区间的不同结构，首先定义状态s_i的下一状态下标sUcc(i)如下：有循环无穷区间中逻辑公式到命题公式的等价转换规则：(2).${(⫬f)}_{(i,k,l)}\stackrel{\mathrm{def}}{=}⫬f_{(i,k,l)};$      (3).(4).(5).${\left(\mathrm{Of}\right)}_{(i,k,l)}\stackrel{\mathrm{def}}{=}{f}_{(\mathrm{succ}\left(i\right),k,l)};$无循环有穷区间中逻辑公式到命题公式的等价转换规则：1).$p_{(i,k)}\stackrel{\mathrm{def}}{=}p\left(s_i\right);$       2).${(⫬f)}_{(i,k)}\stackrel{\mathrm{def}}{=}⫬f_{(i,k)};$3).4).5).${\left(\mathrm{Of}\right)}_{(i,k)}\stackrel{\mathrm{def}}{=}{f}_{(i+1,k)};$      6).$f_{(k+1,k)}\stackrel{\mathrm{def}}{=}\mathrm{false};$PPTL公式正则形中出现的empty和more在有循环的无穷区间和无循环的有穷区间中转换为命题公式的转换规则是相同的，定义如下：其中p，f，g均为命题投影时序逻辑PPTL公式，p是原子命题，f和g是PPTL公式，O是命题投影时序逻辑PPTL公式操作符，empty，more是命题投影时序逻辑PPTL的关键字，empty_(l，k，l)和more_(i,k，l)是限界模型检测中有循环无穷区间下empty和more的表示，empty_(l，k)和more_(i，k)是限界模型检测中无循环有穷区间下empty和more的表示，下标i是当前状态s_i的下标，下标k是限界模型检测的界限k，下标l表示循环的开始状态s_l的下标；步骤4.3.将步骤4.1和步骤4.2得到的约束条件M_k和X_k的等价命题公式合并，得到PPTL限界模型检测问题的形式化描述：及其等价命题公式F，完成限界模型检测问题向SAT问题的转换；步骤5.使用SAT求解器对SAT问题进行求解：有解，说明待验证系统M不满足性质P，给出相应的反例；无解，说明待验证系统Mk‑有界满足性质P，再增大界限k的值，跳至步骤3，进入下一个限界模型检测周期，直到k的值足够大并且在每个限界模型检测周期内待验证系统M都是k‑有界满足性质P的，认为待验证系统M满足性质P，结束限界模型检测过程；其中的SAT问题是否有解说明了系统是否有界满足性质，具体描述如下：利用SAT求解器对F求解，有解，命题公式F可满足，在搜索长度k以内，待验证系统M中存在一条路径使成立，即存在一条违反性质P的路径，待验证系统M不满足性质P，根据命题公式F的解产生违反性质P的路径；无解，命题公式F不可满足，待验证系统M有界满足性质P，在待验证系统M有界满足性质P的情况下，待验证系统是否满足性质是不确定的，再增大界限k的值，进入下一个限界模型检测周期，寻找隐藏更深的错误，当k的值足够大并且待验证系统M总是k‑有界满足性质P，则认为待验证系统满足性质，结束限界模型检测的过程。