基于Stuttering等价技术的有界模型检测的优化

Optimization of Bounded Model Checking Based on Stuttering Equivalence Technology

在讨论有界模型检测及其转换公式的基础上,对有界模型检测转换公式[[M,f]]k中的[[M]]k进行优化。通过在LTL有界模型检测中引入Stuttering等价技术,对状态转换路径优化,避免了SAT求解工具在有界Stuttering等价路径中的重复搜索。以安全系统验证为例,通过两个重要的模态算子G(p)和G(p→F(q)),验证优化方法,实验结果表明,该方法有效地提高了对安全系统保密性和认证性验证的效率。

Based on the discussion of bounded model checking and conversion formula,formula k of bounded model checking＇s conversion formula k is optimized.Through introducing Stuttering equivalence testing technology into LTL bounded model checking,the optimization of states transition path avoids searching repeatedly of SAT Solver in bounded Stuttering equivalent paths.Verification of security systems as an example,optimization method is been validated by two important modal operator G（p） and G（p→F（q））,experimental results show that this method can improve the efficiency of verification for the security and authentication of the system.