计算机科学 ›› 2013, Vol. 40 ›› Issue (Z6): 99-102.

• 智能算法与优化 • 上一篇    下一篇

改进的验证正确性ACTL性质的限界模型检测方法

徐亮,余建平   

  1. 湖南师范大学数学与计算机科学学院 长沙410081高性能计算与随机信息处理省部共建教育部重点实验室 长沙410081;湖南师范大学数学与计算机科学学院 长沙410081高性能计算与随机信息处理省部共建教育部重点实验室 长沙410081
  • 出版日期:2018-11-16 发布日期:2018-11-16
  • 基金资助:
    本文受国家自然科学基金项目(60903168),湖南省自然科学基金项目(12JJ6063),湖南省科技计划项目(2012FJ6012),长沙市科技计划项目(K1109020-11),湖南省重点学科建设项目(湘教发[2011]76号)资助

Improved Bounded Model Checking on Verification of Valid ACTL Properties

XU Liang and YU Jian-ping   

  • Online:2018-11-16 Published:2018-11-16

摘要: 近些年来,基于SAT的限界模型检测方法作为基于BDD的限界模型检测方法的一种有效补充,已经得到了一定的发展。其中,大部分的研究成果都集中在了使用该方法来进行系统查错方面,而在正确性性质的验证上一直难有突破,原因在于正确性性质的验证依赖于一个完备上界,而这个完备上界在限界模型检测方法中很难实现。对传统限界模型检测中的编码方式进行相应改变,就能够在一定程度上解决这一问题,进行正确性性质的验证。在此基础上对该编码方法进行改进,从而提高它的求解效率,扩大其应用领域。

关键词: 限界模型检测,可满足性求解,全局计算树逻辑,验证

Abstract: SAT-based bounded model checking has been introduced as a complementary technique to BDD-based symbolic model checking in recent years,and a lot of successful work has been done with this approach.The success is mostly due to the efficiency of error-detection.Verification of valid properties depends on a completeness threshold that could be too large to be practical.In order to check the valid ACTL properties,the encodings in traditional bounded model checking should be changed.Also,some improvements have been done for this method to improve its efficiency and enlarge its application fields.

Key words: Bounded model checking,SAT,ACTL,Verification

[1] Clarke E M,Emerson A.Design and synthesis of synchronization skeletons using branching-time temporal logic [C]∥Lecture Notes in Computer Science.1981,131:52-71
[2] Clarke E M,Grunberg O,Peled D A.Model Checking [M].MIT Press,1999
[3] Biere A,Cimatti A,Clarke E,et al.Symbolic model checkingwithout BDDs [C]∥Proc.of TACAS 99.1999:193-207
[4] Biere A,Cimatti A,Clarke E,et al.Symbolic Model Checking using SAT procedures instead of BDDs [C]∥Proc.of DAC 99.1999:317-320
[5] Bryant R E.Graph-based algorithms for Boolean function manipulation [J].IEEE Transactions on Computers,1986,35(12):1035-1044
[6] McMillan K L.Symbolic Model Checking [M].Kluwer Academic Publishers,Boston,1993
[7] Coudert O,Madre J C.A unified framework for the formal verification of sequential circuits [C]∥Proc.ICCAD 90.1990:126-129
[8] Emerson E A,Clarke E M.Using branching-time temporal logics to synthesize synchronization skeletons [J].Science of Computer Programming,1982,2(3):241-266
[9] Penczek W,Wozna B,Zbrzezny A.Bounded Model Checking for the Universal Fragment of CTL [J].Fundamenta Informaticae,2002,51(1/2):135-156
[10] Zhang Wen-hui.Verification of ACTL Properties by BoundedModel Checking [C]∥EUROCAST 2007.Lecture Notes in Computer Science.2007,4739:556-563
[11] Xu Yan-yan,Chen Wei,Xu Liang,et al.Evaluation of SAT-based Bounded Model Checking of ACTL Properties [C]∥Proceedings of the 1st Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering.2007:339-348
[12] Xu Liang,Chen Wei,Xu Yan-yan,et al.Improved BoundedModel Checking for Universal Fragment of CTL [J].Journal of Computer Science and Technology,2009,24(1):96-109
[13] 徐亮.限界模型检测方法及其应用[D].北京:中国科学院研究生院,2009
[14] Pieprzyk J,Qu Cheng-xin.Rotation-Symmetric Functions andFast Hashing [C]∥Proc.of ACISP 98.1998:169-180
[15] de Moura L,Ruess H,Sorea M.Bounded Model Checking and Induction:From Refutation to Verification [C]∥Proc.of CAV 2003.2003:14-26
[16] Jhala R,McMillan K L.Interpolation and SAT-Based ModelChecking [C]∥Proc.of CAV 2003.2003:1-13
[17] Xu Liang.SMT-based Bounded Model Checking for Real-time Systems [C]∥Proceedings of the Eighth International Conference on Quality Software.2008:120-125
[18] Xu Liang.Improved SMT-based Bounded Model Checking forReal-time Systems [J].Journal of Software,2010,21(7):1491-1502

No related articles found!
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!