×

Lazy slicing for state-space exploration. (English) Zbl 1280.68123

Summary: CEGAR (counterexample-guided abstraction refinement)-based slicing is one of the most important techniques in reducing the state space in model checking. However, CEGAR-based slicing repeatedly explores the state space handled previously in case a spurious counterexample is found. Inspired by lazy abstraction, we introduce the concept of lazy slicing which eliminates this repeated computation. Lazy slicing is done on-the-fly, and only up to the precision necessary to rule out spurious counterexamples. It identifies a spurious counterexample by concretizing a path fragment other than the full path, which reduces the cost of spurious counterexample decision significantly. Besides, we present an improved over-approximate slicing method to build a more precise slice model. We also provide the proof of the correctness and the termination of lazy slicing, and implement a prototype model checker to verify safety property. Experimental results show that lazy slicing scales to larger systems than CEGAR-based slicing methods.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)

Software:

SPIN
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Clarke E M, Grunberg O, Peled D A. Model Checking. Cambridge, Massachusetts: The MIT Press, 1999, pp.5–19.
[2] Clarke E M, Emerson E A, Sifakis J. Model checking: Algorithmic verification and debugging. Commun. ACM, 2009, 52(11): 74–84. · Zbl 05748004 · doi:10.1145/1592761.1592781
[3] Weiser M. Program slicing. In Proc. the 5th Int. Conf. Software Engineering, March 1981, pp.439–449.
[4] Brückner I, Wehrheim H. Slicing an integrated formal method for verification. In Proc. ICFEM, Nov. 2005, pp.360–374. · Zbl 1118.68541
[5] Clarke E M, Fujita M, Rajan S P, Reps T W, Shankar S, Teitelbaum T. Program slicing of hardware description languages. In Proc. the 10th IFIP WG 10.5 Advanced Research Working Conf. Correct Hardware Design and Verification Methods, September 1999, pp.298–312.
[6] Hatcliff J, Dwyer M B, Zheng H. Slicing software for model construction. Higher-Order Symbol. Comput., 2000, 13(4): 315–353. · Zbl 0972.68021 · doi:10.1023/A:1026599015809
[7] Yatapanage N, Winter K, Zafar S. Slicing behavior tree models for verification. In Proc. the 6th IFIP Int. Conf. Theoretical Computer Science, September 2010, pp.125–139. · Zbl 1202.68258
[8] Dwyer M B, Hatclifi J, Hoosier M, Ranganath V, Robby, Wallentine T. Evaluating the effectiveness of slicing for model reduction of concurrent object-oriented programs. In Proc. the 12th TACAS, March 25-April 2, 2006, pp.73–89.
[9] Godefroid P. Using partial orders to improve automatic verification methods. InProc. the 2nd International Workshop on Computer Aided Verification, June 1990, pp.176–185. · Zbl 0765.68122
[10] Emerson E A, Sistla A P. Symmetry and model checking. Formal Methods in System Design, 1996, 9(1): 10–131.
[11] Miller A, Donaldson A, Calder M. Symmetry in temporal logic model checking. ACM Computing Surveys (CSUR), 2006, 38(3): Article No.8.
[12] Heitmeyer C, Kirby J, Labaw B, Archer M, Bharadwaj R. Using abstraction and model checking to detect safety violations in requirements specifications. IEEE Transactions on Software Engineering, 1998, 24(11): 927–948. · Zbl 05114716 · doi:10.1109/32.730543
[13] Bharadwaj R, Heitmeyer C L. Model checking complete requirements specifications using abstraction. Automated Software Engineering, 1999, 6(1): 37–68. · Zbl 05468935 · doi:10.1023/A:1008697817793
[14] Hong H S, Lee I, Sokolsky O. Abstract slicing: A new approach to program slicing based on abstract interpretation and model checking. In Proc. the 15th SCAM 2005, September 30-Oct.1, 2005, pp.25–34.
[15] Brückner I, Dräger K, Finkbeiner B, Wehrheim H. Slicing abstractions. Fundam. Inf., 2008, 89(4): 369–392. · Zbl 1154.68079
[16] Holzmann G J. Personal Communication. Oct. 2005.
[17] Clarke E M, Grumberg O, Jha S, Lu Y, Veith H. Counterexample-guided abstraction refinement for symbolic model checking. J. ACM, 2003, 50(5): 752–794. · Zbl 0974.68517 · doi:10.1145/876638.876643
[18] Wehrheim H. Incremental slicing. In Proc. the 8th ICFEM 2006, November 2006, pp.514–528.
[19] Sabouri H, Sirjani M. Slicing-based reductions for rebeca. Electronic Notes in Theoretical Computer Science, 2010, 260(1): 209–224. · Zbl 1214.68223 · doi:10.1016/j.entcs.2009.12.039
[20] Henzinger T A, Jhala R, Majumdar R, Sutre G. Lazy abstraction. In Proc. the 29th ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages, Jan. 2002, pp.58–70. · Zbl 1323.68374
[21] Graf S, Saïdi H. Construction of abstract state graphs with PVS. In Proc. the 9th CAV, June 1997, pp.72–83.
[22] Jung Y, Kong S, Wang B, Yi K. Deriving invariants by algorithmic learning, decision procedures, and predicate abstraction. In Proc. the 11th Int. Conf. Verification, Model Checking, and Abstract Interpretation, January 2010, pp.180–196. · Zbl 1248.68272
[23] Podelski A, Wies T. Counterexample-guided focus. In Proc. the 37th POPL, Jan. 2010, pp.249–260. · Zbl 1312.68067
[24] Tonetta S. Abstract model checking without computing the abstraction. In Proc. the 2nd World Congress on Formal Methods, November 2009, pp.89–105.
[25] Baier K CJ, Principles of Model Checking. Cambridge, Massachusetts: The MIT Press, 2008, pp.468–595.
[26] Groce A, Kroening D, Lerda F. Understanding counterexamples with explain. In Proc. the 16th International Conference on Computer Aided Verification, July 2004, pp.453–456. · Zbl 1103.68620
[27] Gastin P, Moro P, Zeitoun M. Minimization of counterexamples in SPIN. In Proc. the 11th International SPIN Workshop on Model Checking Software, April 2004, pp.92–108. · Zbl 1125.68369
[28] Beer I, Ben-David S, Chockler H, Orni A, Treffer R. Explaining counterexamples using causality. In Proc. the 21st CAV, June 26-July 2, 2009, pp.94–108. · Zbl 1242.68150
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.