基于SPIN的LTL属性分解方法研究

STUDY ON SPIN-BASED LTL PROPERTY DECOMPOSITION

提出一种基于模型检测工具SPIN的LTL属性分解方法以解决状态空间爆炸问题。根据逻辑和时序操作符常见的组合情况,讨论不同的属性分解模式,根据子属性构建的切片准则进行程序切片,利用SPIN对切片后的等价简化模型进行检测,从而将对原模型上属性的检测转化成对复杂度较低的子模型上各子属性的分别检测。实验结果表明,该方法具有一定的有效性。

To solve the state space explosion problem, we propose a linear temporal logic （LTL） property decomposition method which is based on model check tool SPIN. According to the common combinations of logic and temporal operators, we discuss different property decomposition patterns, slice the programs according to the slicing criteria constructed by sub-property, and then employ SPIN to check the sliced equivalent simplified models, so that convert the check on the property of the original model to the respective checks on each sub- property of sub-model with lower complexity. Experimental results show that the method is valid to certain extent.