| 改进的验证正确性ACTL性质的限界模型检测方法 |
| |
| 引用本文： | 徐亮,余建平.改进的验证正确性ACTL性质的限界模型检测方法[J].计算机科学,2013,40(Z6):99-102. |
| |
| 作者姓名： | 徐亮 余建平 |
| |
| 作者单位： | 湖南师范大学数学与计算机科学学院 长沙410081高性能计算与随机信息处理省部共建教育部重点实验室 长沙410081;湖南师范大学数学与计算机科学学院 长沙410081高性能计算与随机信息处理省部共建教育部重点实验室 长沙410081 |
| |
| 基金项目： | 本文受国家自然科学基金项目(60903168),湖南省自然科学基金项目(12JJ6063),湖南省科技计划项目(2012FJ6012),长沙市科技计划项目(K1109020-11),湖南省重点学科建设项目(湘教发[2011]76号)资助 |
| |
| 摘 要： | 近些年来,基于SAT的限界模型检测方法作为基于BDD的限界模型检测方法的一种有效补充,已经得到了一定的发展。其中,大部分的研究成果都集中在了使用该方法来进行系统查错方面,而在正确性性质的验证上一直难有突破,原因在于正确性性质的验证依赖于一个完备上界,而这个完备上界在限界模型检测方法中很难实现。对传统限界模型检测中的编码方式进行相应改变,就能够在一定程度上解决这一问题,进行正确性性质的验证。在此基础上对该编码方法进行改进,从而提高它的求解效率,扩大其应用领域。
|
| 关 键 词： | 限界模型检测 可满足性求解 全局计算树逻辑 验证 |
Improved Bounded Model Checking on Verification of Valid ACTL Properties |
| |
| XU Liang and YU Jian-ping.Improved Bounded Model Checking on Verification of Valid ACTL Properties[J].Computer Science,2013,40(Z6):99-102. |
| |
| Authors: | XU Liang and YU Jian-ping |
| |
| Affiliation: | College of Mathematics and Computer Science,Hunan Normal University,Changsha 410081,China Key Laboratory of High Performance Computing and Stochastic Information Processing,Ministry of Education of China,Changsha 410081,China;College of Mathematics and Computer Science,Hunan Normal University,Changsha 410081,China Key Laboratory of High Performance Computing and Stochastic Information Processing,Ministry of Education of China,Changsha 410081,China |
| |
| Abstract: | |
| |
| Keywords: | Bounded model checking SAT ACTL Verification |
|
| 点击此处可从《计算机科学》浏览原始摘要信息 |
|
点击此处可从《计算机科学》下载全文 |
|
