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

• 作者: 曾庆凯 贺志宏
• 来源期刊: 计算机应用与软件
• 学科: 工学
• 关键词: 线性时序逻辑属性 模型检测 属性分解 静态程序切片
• 年，卷（期）: 2014,（7）
• 所属期刊栏目: 应用技术与研究
• 页码范围: 43-46,65
• 页数: 5页
• 分类号: TP309
• 字数: 4688字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-386x.2014.07.012

摘要

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