|
|||||
|
|
| 有界模型检测的优化 | |
| 引用本文： | 杨晋吉,苏开乐,骆翔宇,林瀚,肖茵茵.有界模型检测的优化[J].软件学报,2009,20(8):2005-2014. |
| 作者姓名： | 杨晋吉 苏开乐 骆翔宇 林瀚 肖茵茵 |
| 作者单位： | 1. 华南师范大学,计算机学院,广东,广州,510631;中山大学,信息科学与技术学院,广东,广州,510275 2. 北京大学,信息科学技术学院,北京,100871 3. 桂林电子科技大学,计算机与控制学院,广西,桂林,541004 4. 中山大学,信息科学与技术学院,广东,广州,510275 |
| 基金项目： | 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 (广东省科技攻关项目) |
| 摘 要： | 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中验证其他模态算子时的编码优化也有参考价值. |
| 关 键 词： | 模型检测 有界模型检测 可满足性问题 模态算子 递推公式 |
| 收稿时间： | 2007/9/29 0:00:00 |
| 修稿时间： | 2008/4/15 0:00:00 |
Optimization of Bounded Model Checking |
|
| YANG Jin-Ji,SU Kai-Le,LUO Xiang-Yu,LIN Han and XIAO Yin-Yi.Optimization of Bounded Model Checking[J].Journal of Software,2009,20(8):2005-2014. | |
| Authors: | YANG Jin-Ji SU Kai-Le LUO Xiang-Yu LIN Han and XIAO Yin-Yi |
| Affiliation: | School of Computer;South China Normal University;Guangzhou 510631;China;School of Information Science and Technology;Sun Yat-Sen University;Guangzhou 510275;China;School of Electronics Engineering and Computer Science;Peking University;Beijing 100871;China;College of Computer and Control;Guilin University of Electronic Technology;Guilin 541004;China |
| Abstract: | |
| Keywords: | model checking bounded model checking SAT (satisfiability) modal operator recursion formula |
| 本文献已被 CNKI 万方数据 等数据库收录！ | |
| 点击此处可从《软件学报》浏览原始摘要信息 | |
| 点击此处可从《软件学报》下载全文 | |