基于SAT的软件验证

• 作 者: 周从华 陈振宇 鞠时光
• 机 构: 江苏大学计算机科学与通信工程学院
• 出 处: 计算机研究与发展
• 发表日期: 2008年z1期
• 关键词: 模型检测 SAT 软件验证 形式化分析
• 基金项目: 国家自然科学基金项目(60603041);江苏省自然科学基金项目(BK2006073);江苏大学高级人才科研启动基金项目(07JDG014)

线性时态逻辑SE-LTL是具有高表达力和基于状态、事件推理能力的并发系统规约语言.目前,SE-LTL的模型检测算法依然是显式的,状态空间爆炸是检测的主要困难.对SE-LTL引入一种有界模型检测技术,该技术将SE-LTL模型检测归约为命题公式的可满足性问题,避免了基于二叉图方法中状态空间的快速增长,加速了验证过程.对SE-LTL-X进一步在该技术中集成stuttering等价技术.实验结果表明该集成有效地降低了验证时间.