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

STUDY ON SPIN-BASED LTL PROPERTY DECOMPOSITION

作　　者：贺志宏[1] 曾庆凯[2] 

机构地区：[1]南京大学计算机软件新技术国家重点实验室,江苏南京210046 [2]南京大学计算机科学与技术系,江苏南京210046

出　　处：《计算机应用与软件》2014年第7期43-46,65,共5页Computer Applications and Software

基　　金：国家自然科学基金项目(61170070);国家科技支撑计划项目(2012BAK26B01);国家高技术研究发展计划项目(2011AA1A202)

摘　　要：提出一种基于模型检测工具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.

关 键 词：线性时序逻辑属性 模型检测 属性分解 静态程序切片 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]