主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2018-2019年专刊出版计划 微信服务介绍 最新一期:2019年第10期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
杨晋吉,苏开乐,骆翔宇,林瀚,肖茵茵.有界模型检测的优化.软件学报,2009,20(8):2005-2014
有界模型检测的优化
Optimization of Bounded Model Checking
投稿时间:2007-09-29  修订日期:2008-04-15
DOI:
中文关键词:  模型检测  有界模型检测  可满足性问题  模态算子  递推公式
英文关键词:model checking  bounded model checking  SAT (satisfiability)  modal operator  recursion formula
基金项目:Supported by the Outstanding Young Research Fund of China under Grant No.60725207 (国家杰出青年基金); the National Natural Science Foundation of China under Grant Nos.60473004, 60763004 (国家自然科学基金); the Guangdong Provincial Natural Science Foundation of China under Grant No.06023195 (广东省自然科学基金), the Guangdong Provincial Research Foundation of Science and Technology of China under Grant No.2007B010400068 (广东省科技攻关项目)
作者单位
杨晋吉 华南师范大学 计算机学院,广东 广州 510631
中山大学 信息科学与技术学院,广东 广州 510275 
苏开乐 北京大学 信息科学技术学院,北京 100871 
骆翔宇 桂林电子科技大学 计算机与控制学院,广西 桂林 541004 
林瀚 中山大学 信息科学与技术学院,广东 广州 510275 
肖茵茵 中山大学 信息科学与技术学院,广东 广州 510275 
摘要点击次数: 4248
全文下载次数: 4261
中文摘要:
      G(p)和G(p→F(q))是有界模型检测(bounded model checking,简称BMC)中的两个重要的常用模态算子.对验证G(p)和G(p→F(q))编码转换公式进行优化.通过分析当验证这些模态算子时FSM(finite state machine)的状态转移和线性时序逻辑(linear-time temporal logic,简称LTL)的语义特征.在现有的编码公式的基础上,给出了简洁、高效的递推公式,该公式有利于高效编码成SAT(satisfiability)实例;证明了递推公式和原转换公式的逻辑关系.通过实验比较分析,在生成SAT实例规模和易求解方面都优于BMC中求解这些模态算子的现有的两种重要方法AA_BMC和Timo_BMC.所给出的方法和思想对于BMC中验证其他模态算子时的编码优化也有参考价值.
英文摘要:
      This paper optimizes the encoding of verifying G(p) and G(p→F(q)) which are two important and frequently used modal operators in optimization of encoding for bounded model checking (BMC). Through analysis of the properties of finite state machine (FSM) and LTL (linear-time temporal logic) when verifying these modal operators, it presents a concise recursive formula, which can efficiently translate BMC instances into SAT (satisfiability) instances. The logical properties of these recursion formulas are verified. The experimental comparison between the optimization of BMC and the other two important methods AA_BMC and Timo_BMC for solving these modal operators in BMC shows that the former is superior to the latter in both the scale of instances and the difficulty to solve the problem. Research of this paper is also beneficial to encoding optimization of verifying other modal operators in BMC.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会 京ICP备05046678号-4
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利