| | This Article | |
| |
| |
| | Share | |
| |
| |
| | Bibliographic References | |
| |
| |
| | Add to: | |
| |
 Digg
 Furl
 Spurl
 Blink
 Simpy
 Google
 Del.icio.us
 Y!MyWeb
| |
| | Search | |
| |
| |
| | |
Integrating Evolutionary Computation with Abstraction Refinement for Model Checking
January 2010 (vol. 59 no. 1)
pp. 116-126
Fei He, Tsinghua University, Beijing
Ming Gu, Tsinghua University, Beijing
Model checking for large-scale systems is extremely difficult due to the state explosion problem. Creating useful abstractions for model checking task is a challenging problem, often involving many iterations of refinement. In this paper we consider techniques for model checking in the counterexample-guided abstraction refinement. The state separation problem is one popular approach in counterexample-guided abstraction refinement, and it poses the main hurdle during the refinement process. To achieve effective minimization of the separation set, we present a novel probabilistic learning approach based on the sample learning technique, evolutionary algorithm, and effective heuristics. We integrate it with the abstraction refinement framework in the VIS [1] model checker. We include experimental results on model checking to compare our new approach to recently published techniques. The benchmark results show that our approach has overall speedup of more than 56 percent against previous techniques. Our work is the first successful integration of evolutionary algorithm and abstraction refinement for model checking.
[1] R.K. Brayton, G.D. Hachtel, A. Sangiovanni-Vincentelli, F. Somenzi, A. Aziz, S.-T. Cheng, S. Edwards, S. Khatri, Y. Kukimoto, A. Pardo, S. Qadeer, R.K. Ranjan, S. Sarwary, T.R. Shiple, G. Swamy, and T. Villa, “VIS: A System for Verification and Synthesis,” Proc. Eighth Int'l Conf. Computer-Aided Verification (CAV), R. Alur and T.A. Henzinger, eds., vol. 1102, pp. 428-432, 1996.
[2] W.N.N. Hung and N. Narasimhan, “Reference Model Based RTL Verification: An Integrated Approach,” Proc. IEEE Int'l High Level Design Validation and Test Workshop (HLDVT), pp. 9-13, Nov. 2004.
[3] R.H. Beers, R. Ghughal, and M.D. Aagaard, “Applications of Hierarchical Verification in Model Checking,” Proc. Formal Methods in Computer-Aided Design, Nov. 2000.
[4] E.M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith, “Counterexample-Guided Abstraction Refinement,” Proc. Computer-Aided Verification, pp. 154-169, 2000.
[5] E.M. Clarke, A. Gupta, and O. Strichman, “SAT Based Counterexample-Guided Abstraction-Refinement,” IEEE Trans. Computer Aided Design, vol. 23, no. 7, pp. 1113-1123, July 2004.
[6] C. Wang, B. Li, H. Jin, G.D. Hachtel, and F. Somenzi, “Improving Ariadne's Bundle by Following Multiple Threads in Abstraction Refinement,” IEEE Trans. Computer Aided Design, vol. 25, no. 11, pp. 2297-2316, Nov. 2006.
[7] R.P. Kurshan, Computer Aided Verification of Coordinating Processes. Princeton Univ. Press, 1994.
[8] W. Lee, A. Pardo, J. Jang, G. Hachtel, and F. Somenzi, “Tearing Based Abstraction for CTL Model Checking,” Proc. Int'l Conf. Computer-Aided Design, pp. 76-81, Nov. 1996.
[9] J. Lind-Nielsen and H.R. Andersen, “Stepwise CTL Model Checking of State/Event Systems,” Proc. Computer-Aided Verification, pp. 316-327, 1999.
[10] A. Pardo and G.D. Hachtel, “Incremental CTL Model Checking Using BDD Subsetting,” Proc. Design Automation Conf., pp. 457-462, 1998.
[11] E.M. Clarke, A. Gupta, J.H. Kukula, and O. Strichman, “SAT Based Abstraction-Refinement Using ILP and Machine Learning Techniques,” Proc. Computer-Aided Verification (CAV), E. Brinksma and K.G. Larsen, eds., pp. 265-279, 2002.
[12] P. Chauhan, E.M. Clarke, J. Kukula, S. Sapra, H. Veith, and D. Wang, “Automated Abstraction Refinement for Model Checking Large State Spaces Using SAT Based Conflict Analysis,” Proc. Formal Methods in Computer-Aided Design (FMCAD), 2002.
[13] T.A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre, “Lazy Abstraction,” Proc. Symp. Principles of Programming Languages, pp.58-70, 2002.
[14] M. Glusman, G. Kamhi, S. Mador-Haim, R. Fraer, and M.Y. Vardi, “Multiple-Counterexample Guided Iterative Abstraction Refinement: An Industrial Evaluation,” Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 176-191, 2003.
[15] S.G. Govindaraju and D.L. Dill, “Counterexample-Guided Choice of Projections in Approximate Symbolic Model Checking,” Proc. Int'l Conf. Computer-Aided Design (ICCAD), pp. 115-119, 2000.
[16] F. He, X. Song, M. Gu, and J. Sun, “Effective Heuristics for Counterexample-Guided Abstraction Refinement,” Proc. 17th ACM Great Lakes Symp. Very Large-Scale Integration (GLSVLSI '07), H. Zhou and E. Macii, eds., pp. 393-398, 2007.
[17] K.L. McMillan and N. Amla, “Automatic Abstraction without Counterexamples,” Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 2-17, 2003.
[18] A. Gupta and O. Strichman, “Abstraction Refinement for Bounded Model Checking,” Proc. Computer-Aided Verification, K. Etessami and S.K. Rajamani, eds., pp. 112-124, 2005.
[19] A. Gupta, M.K. Ganai, Z. Yang, and P. Ashar, “Iterative Abstraction Using SAT-Based BMC with Proof Analysis,” Proc. Int'l Conf. Computer-Aided Design (ICCAD), pp. 416-423, 2003.
[20] C. Wang, H. Jin, G.D. Hachtel, and F. Somenzi, “Refining the SAT Decision Ordering for Bounded Model Checking,” Proc. Design Automation Conf. (DAC), pp. 535-538, 2004.
[21] S. Graf and H. Saïdi, “Construction of Abstract State Graphs with PVS,” Proc. Computer-Aided Verification, pp. 72-83, 1997.
[22] H. Jain, D. Kroenig, N. Sharygina, and E.M. Clarke, “Word Level Predicate Abstraction and Refinement for Verifying RTL Verilog,” Proc. Design Automation Conf., pp. 445-450, 2005.
[23] P.-H. Ho, T. Shiple, K. Harer, J.H. Kukula, R. Damiano, V. Bertacco, J. Taylor, and J. Long, “Smart Simulation Using Collaborative Formal Simulation Engines,” Proc. Int'l Conf. Computer-Aided Design, pp. 120-126, 2000.
[24] D. Wang, P.-H. Ho, J. Long, J.H. Kukula, Y. Zhu, T. Ma, and R. Damiano, “Formal Property Verification by Abstraction Refinement with Formal, Simulation and Hybrid Engines,” Proc. Design Automation Conf., pp. 35-40, 2001.
[25] F. He, X. Song, M. Gu, and J. Sun, “A Probabilistic Learning Approach for Counterexample Guided Abstraction Refinement,” Proc. Fourth Int'l Symp. Automated Technology for Verification and Analysis (ATVA '06), S. Graf and W. Zhang, eds., pp. 29-50, Oct. 2006.
[26] T.H. Cormen, C.E. Leiserson, R.L. Rivest, and C. Stein, Introduction to Algorithms, second ed. MIT Press/McGraw-Hill, 2001.
[27] D. Dumitrescu, B. Lazzerini, L. Jain, and A. Dumitrescu, Evolutionary Computation, L. Jain, ed. CRC Press, 2000.
[28] J. Beasley and P. Chu, “A Genetic Algorithm for the Set Covering Problem,” European J. Operational Research, vol. 94, pp. 392-404, 1996.
[29] S. Sen, “Minimal Cost Set Covering Using Probabilistic Methods,” Proc. 1993 ACM/SIGAPP Symp. Applied Computing, pp. 157-164, 1993.
[30] U. Aickelin, “An Indirect Genetic Algorithm for Set Covering Problems,” J. Operational Research Soc., vol. 53, no. 10, pp. 1118-1126, 2002.
[31] E. Marchiori and A. Steenbeek, “An Evolutionary Algorithm for Large Scale Set Covering Problems with Application to Airline Crew Scheduling,” Proc. EvoWorkshops, pp. 367-381, 2000.
[32] G. Syswerda, “Uniform Crossover in Genetic Algorithms,” Proc. Third Int'l Conf. Genetic Algorithms, pp. 2-9, 1989.
[33] W.M. Spears and K.A. De Jong, “On the Virtues of Parameterized Uniform Crossover,” Proc. Fourth Int'l Conf. Genetic Algorithms, R.Belew and L. Booker, eds., pp. 230-236, http://citeseer.ist.psu. eduspears91virtues.html , 1991.
[34] VIS Verification Benchmarks, ftp://vlsi.colorado.edu/pub/visvis-verilog-models-1.0.tar.gz , 2008.
Index Terms:
Formal models, verification.
Citation:
Fei He, Xiaoyu Song, William N.N. Hung, Ming Gu, Jiaguang Sun, "Integrating Evolutionary Computation with Abstraction Refinement for Model Checking," IEEE Transactions on Computers, vol. 59, no. 1, pp. 116-126, Jan. 2010, doi:10.1109/TC.2009.105
