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

发布时间：2018-10-23 10:11

【摘要】：提出一种基于模型检测工具SPIN的LTL属性分解方法以解决状态空间爆炸问题。根据逻辑和时序操作符常见的组合情况,讨论不同的属性分解模式,根据子属性构建的切片准则进行程序切片,利用SPIN对切片后的等价简化模型进行检测,从而将对原模型上属性的检测转化成对复杂度较低的子模型上各子属性的分别检测。实验结果表明,该方法具有一定的有效性。
[Abstract]:A LTL attribute decomposition method based on model checking tool SPIN is proposed to solve the problem of state space explosion. According to the common combination of logic and sequential operators, different attribute decomposition modes are discussed. The program slicing is carried out according to the slicing criterion constructed by subattributes, and the equivalent simplified model after slicing is detected by SPIN. Thus, the detection of attributes on the original model is transformed into the detection of each subattribute on the submodel with lower complexity. Experimental results show that the method is effective.
【作者单位】： 南京大学计算机软件新技术国家重点实验室;南京大学计算机科学与技术系;
【基金】：国家自然科学基金项目(61170070) 国家科技支撑计划项目(2012BAK26B01) 国家高技术研究发展计划项目(2011AA1A202)
【分类号】：TP306

【参考文献】

相关期刊论文 前2条

1 李兴锋;张新常;杨美红;阎保平;;基于SPIN的模块化模型检测方法研究[J];电子与信息学报;2011年04期

2 戎玫;何志学;张广泉;;一种基于LTL性质的面向对象并发程序切片方法[J];计算机应用;2008年05期

【共引文献】

相关期刊论文 前3条

1 高洪博;李清宝;王炜;朱瑜;;基于敏感位置识别的状态化简技术研究[J];电子与信息学报;2013年03期

2 钱成;燕雪峰;周勇;徐海生;;基于状态约简的顺序图和状态图一致性检测[J];计算机应用研究;2014年05期

3 王曦;徐中伟;;基于启发式NDFS的模型检测新算法[J];小型微型计算机系统;2012年08期

相关博士学位论文 前1条

1 高洪博;指令诱发型硬件木马检测技术研究[D];解放军信息工程大学;2013年

相关硕士学位论文 前1条

1 秦英;VoIP数据流的可信传输及其安全属性的形式化验证[D];北京交通大学;2013年

【二级参考文献】

相关期刊论文 前1条

1 董威,王戟,齐治昌;并发程序的切片模型检验方法[J];计算机学报;2003年03期

【相似文献】

相关期刊论文 前10条

1 曾云辉;朱光慧;;基于属性分解的信息安全风险分析与计算模型[J];山东科学;2009年02期

2 余永红;柏文阳;;强制数据隐私和用户隐私的外包数据库服务研究[J];计算机应用研究;2011年01期

3 ;[J];;年期

4 ;[J];;年期

5 ;[J];;年期

6 ;[J];;年期

7 ;[J];;年期

8 ;[J];;年期

9 ;[J];;年期

10 ;[J];;年期

相关硕士学位论文 前1条

1 杨刚;外包数据库机密性保护技术研究[D];解放军信息工程大学;2013年

，

本文编号：2288922