Skip to main content
SpringerLink
Log in

Partial-order reduction and trail improvement in directed model checking

  • Special section on the algorithmics of software model checking
  • Published:
International Journal on Software Tools for Technology Transfer Aims and scope Submit manuscript

Abstract

In this paper we present work on trail improvement and partial-order reduction in the context of directed explicit-state model checking. Directed explicit-state model checking employs directed heuristic search algorithms such as A* or best-first search to improve the error-detection capabilities of explicit-state model checking. We first present the use of directed explicit-state model checking to improve the length of already established error trails. Second, we show that partial-order reduction, which aims at reducing the size of the state space by exploiting the commutativity of concurrent transitions in asynchronous systems, can coexist well with directed explicit-state model checking. Finally, we illustrate how to mitigate the excessive length of error trails produced by partial-order reduction in explicit-state model checking. In this context we also propose a combination of heuristic search and partial-order reduction to improve the length to already provided counterexamples.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Alur R, Brayton R, Henzinger T, Qaderer S, Rajamani S (1997) Partial-order reduction in symbolic state space exploration. In: 9th conference on computer-aided verification (CAV). Lecture notes in computer science, vol 1254. Springer, Berlin Heidelberg New York, pp 340–351

  2. Ball T, Naik M, Rajamani S (2003) From sympton to cause: Localizing errors in counterexample traces. In: 30th annual ACM symposium on principles of programming languages (POPL)

  3. Ball T, Rajamani SK (2001) Automatically validating temporal safety properties of interfaces. In: 7th international SPIN workshop on software model checking. Lecture notes in computer science, vol 2057. Springer, Berlin Heidelberg New York, pp 103–122

  4. Behrmann G, Fehnker A, Hune T, Larsen KG, Petterson P, Romijn J (2001) Guiding and cost-imality in UPPAAL. In: AAAI spring symposium on model-based validation of intelligence, pp 66–74

  5. Behrmann G, Fehnker A, Hune T, Larsen KG, Petterson P, Romijn J, Vaandrager FW (2001) Efficient guiding towards cost-imality in uppaal. In: Conference on tools and algorithms for the construction and analysis of systems (TACAS). Lecture notes in computer science, vol 2031. Springer, Berlin Heidelberg New York

  6. Bérard B, Bidoit M, Finkel A, Laroussinie F, Petit A, Petrucci L, Schnoebelen P (2001) Systems and software verification: model-checking techniques and tools. Springer, Berlin Heidelberg New York

    Google Scholar 

  7. Bloem R, Ravi K, Somenzi F (2000) Symbolic guided search for CTL model checking. In: ACM/IEEE Design Automation Conference (DAC), pp 29–34

  8. Bonet B, Geffner H (2001) Planning as heuristic search. Artif Intell 129(1–2):5–33

  9. Bosnacki D, Dams D, Holenderski L (2000) Symmetric SPIN. In: 7th SPIN workshop on software model checking. Lecture notes in computer science, vol 1885. Springer, Berlin Heidelberg New York, pp 1–19

  10. Chou C-T, Peled D (1996) Formal verification of a partial-order reduction technique for model checking. In: 2nd conference on tools and algorithms for construction and analysis of systems (TACAS). Lecture notes in computer science, vol 1055. Springer, Berlin Heidelberg New York, pp 241–257

  11. Clarke EM, Grumberg O, Peled DA (1999) Model checking. MIT Press, Cambridge, MA

  12. Cobleigh JM, Clarke LA, Osterweil LJ (2001) The right algorithm at the right time: Comparing data flow analysis algorithms for finite state verification. In: 23rd IEEE international conference on software engineering (ICSE), pp 37–46

  13. Cohen JD (1997) Recursive hashing functions for n-grams. ACM Trans Inf Sys 15(3):291–320

    Article  Google Scholar 

  14. Corbett JC, Dwyer MB, Hatcliff J, Laubach S, Pasareanu CS, Robby, Zheng H (2000) Bandera: Extracting finite-state models from Java source code. In: 22nd IEEE international conference on software engineering (ICSE)

  15. Cormen TH, Leiserson CE, Rivest RL (1990) Introduction to algorithms. MIT Press, Cambridge, MA

  16. Dams D, Gerth R, Grumberg O (1997) Abstract interpretation of reactive systems. ACM Trans Programm Lang Sys 19(2):111–149

    Google Scholar 

  17. Dechter R, Pearl J (1985) Generalized best-first strategies and the optimality of A*. J ACM 32

  18. Dolev D, Klawe M, Rodeh M (1982) An O(n log n) unidirectional distributed algorithm for extrema finding in a circle. J Algorithms 3:245–260

    Article  MathSciNet  Google Scholar 

  19. Edelkamp S (1999) Data structures and learning algorithms in state space search. PhD thesis, University of Freiburg, Infix

  20. Edelkamp S (2003) Promela planning. In: 10th SPIN workshop on model checking software. Lecture notes in computer science, vol 2648. Springer, Berlin Heidelberg New York, pp 197–212

  21. Edelkamp S, Leue S, Lluch-Lafuente A (2004) Directed explicit-state model checking in the validation of communication protocols. Int J Softw Tools Technol Transfer 5(2–3):247–267. http://www.di.unipi.it/%7Elafuente/papers/index.html#phd

  22. Edelkamp S, Lluch-Lafuente A, Leue S (2001) Trail-directed model checking. In: Stoller SD, Visser W (eds) Electronic Notes in Theoretical Computer Science, vol 55. Elsevier, Amsterdam

  23. Edelkamp S, Mehler T (2003) Byte code distance heuristics and trail direction for model checking Java programs. In: 2nd workshop on model checking and artificial intelligence, pp 69–76

  24. Emerson EA, Jha S, Peled D (1997) Comibing partial order and symmetry reduction. In: 3rd conference on tools and algorithms for the construction and analysis of systems (TACAS). Lecture notes in computer science, vol 1217. Springer, Berlin Heidelberg New York, pp 19–34

  25. Emerson EA, Sistla AP (1993) Symmetry and model checking. In: 5th international conference on computer-aided verification (CAV). Lecture notes in computer science, vol 697. Springer, Berlin Heidelberg New York, pp 463–378

  26. Godefroid P (1991) Using partial orders to improve automatic verification methods. In: 2nd conference on computer-aided verification (CAV). Lecture notes in computer science, vol 531. Springer, Berlin Heidelberg New York, pp 176–185

  27. Godefroid P, Khurshid S (2002) Exploring very large state spaces using genetic algorithms. In: 8th conference on tools and algorithms for the construction and analysis of systems (TACAS). Lecture notes in computer science, vol 2280. Springer, Berlin Heidelberg New York, pp 266–280

  28. Graf S, Saidi H (1997) Construction of abstract state graphs of infinite systems with PVS. In: 9th conference on computer-aided verification (CAV). Lecture notes in computer science, vol 1254. Springer, Berlin Heidelberg New York

  29. Groce A, Visser W (2002) Heuristic model checking for java programs. In: 9th SPIN workshop on model checking software. Lecture notes in computer science, vol 2318. Springer, Berlin Heidelberg New York, pp 242–245

  30. Groce A, Visser W (2002) Model checking java programs using structural heuristics. In: International symposium on software testing and analysis (ISSTA). ACM Press, New York

  31. Groce A, Visser W (2003) What went wrong: Explaining counterexamples. In: Workshop on software model checking (SPIN). Lecture notes in computer science, vol 2648. Springer, Berlin Heidelberg New York, pp 121–135

  32. Object Management Group (1997) The common object request broker architecture and specification. Revised version 2.1

  33. Hart PE, Nilsson NJ, Raphael B (1968) A formal basis for heuristic determination of minimum path cost. IEEE Trans Sys Sci Cybern 4:100–107

    Article  Google Scholar 

  34. Holzmann GJ (1990) Design and validation of computer protocols. Prentice-Hall, Englewood Cliffs, NJ

  35. Holzmann GJ (1997) The model checker Spin. IEEE Trans Softw Eng 23(5):279–295

    Article  Google Scholar 

  36. Holzmann GJ (2003) The Spin model checker, primer and reference manual. Addison-Wesley, Reading, MA

  37. Holzmann GJ, Godefroid P, Pirottin D (1992) Coverage preserving reduction strategies for reachability analysis. In: 12th international conference on protocol specification, testing, and verification (PSTV)

  38. Holzmann GJ, Smith MH (2002) An automated verification method for distributed systems software based on model extraction. IEEE Trans Softw Eng 28(4):364–377

    Article  Google Scholar 

  39. Ip CN, Dill DL (1996) Better verification through symmetry. Formal Methods Sys Des 9:41–75

    Article  Google Scholar 

  40. Jin H, Ravi K, Somenzi F (2002) Fate and free will in error traces. In: 8th conference on tools and algorithms for the construction and analysis of systems (TACAS). Lecture notes in computer science, vol 2280. Springer, Berlin Heidelberg New York, pp 445–459

  41. Kamel M, Leue S (2000) Formalization and validation of the General Inter-ORB Protocol (GIOP) using PROMELA and SPIN. Int J Softw Tools Technol Transfer 2(4):394–409

    Article  Google Scholar 

  42. Kamel M, Leue S (2000) VIP: A visual editor and compiler for v-Promela. In: 6th conference on tools and algorithms for the construction and analysis of systems (TACAS). Lecture notes in computer science, vol 1785. Springer, Berlin Heidelberg New York, pp 471–486

  43. Korf RE (1985) Depth-first iterative-deepening: An optimal admissible tree search. Artif Intell 27(1):97–109

    Article  MathSciNet  Google Scholar 

  44. Kurshan RP, Levin V, Minea M, Peled D, Yenigun H (1998) Static partial order reduction. In: 4th conference on tools and algorithms for construction and analysis of systems (TACAS). Lecture notes in computer science, vol 1384. Springer, Berlin Heidelberg New York, pp 345–357

  45. Lerda F, Sinha N, Theobald M (2003) Symbolic model checking of software. In: Electronic notes in theoretical computer science, vol 89. Elsevier, Amsterdam

  46. Lluch-Lafuente A (2003) Symmetry reduction and heuristic search for error detection in model checking. In: 2nd workshop on model checking and artificial intelligence (MoChArt), pp 77–86

  47. Lluch-Lafuente A, Leue S, Edelkamp S (2002) Partial order reduction in directed model checking. In: SPIN workshop on model checking software. Lecture notes in computer science, vol 2318. Springer, Berlin Heidelberg New York, pp 112–127

  48. Manna Z, Pnueli A (1992) The temporal logic of reactive and concurrent systems: specification. Springer, Berlin Heidelberg New York

    Google Scholar 

  49. McVitie DG, Wilson LB (1971) The stable marriage problem. Commun ACM 14(7):486–492

    Article  MathSciNet  Google Scholar 

  50. Nalumasu R, Gopalakrishnan G (1997) A new partial order reduction algorithm for concurrent system verification. In: Hardware description languages and their applications (CHDL). Chapman & Hall, London

  51. Nilsson NJ (1980) Principles of artificial intelligence. Tioga, Palo Alto, CA

  52. Pearl J (1985) Heuristics. Addison-Wesley, Reading, MA

  53. Peled DA (1996) Combining partial order reductions with on-the-fly model-checking. Formal Methods Sys Des 8:39–64

    Article  Google Scholar 

  54. Peled DA (1998) Ten years of partial order reduction. In: 10th conference on computer-aided verification (CAV). Lecture notes in computer science, vol 1427. Springer, Berlin Heidelberg New York, pp 17–28

  55. Sharygina N, Peled D (2001) A combined testing and verification approach for software reliability. In: Formal methods of increasing software productivity, internatioanl symposioum of Formal Methods Europe, pp 611–628

  56. Valmari A (1991) A stubborn attack on state explosion. Lecture notes in computer science, vol 531. Springer, Berlin Heidelberg New York, pp 156–165

  57. Wah BW, Shang Y (1995) Study of ida*-style searches. J Tools Artif Intell 3(4):493–523

    Article  Google Scholar 

  58. Yang CH, Dill DL (1998) Validation with guided search of the state space. In: Conference on design automation (DAC), pp 599–604

Download references

Author information

Authors and Affiliations

  1. Fachbereich Informatik, Universität Dortmund, Baroper Str. 301, GB IV, 44221, Dortmund, Germany

    Stefan Edelkamp

  2. Fachbereich Informatik und Informationswissenschaft, Universität Konstanz, 78457, Konstanz, Germany

    Stefan Leue

  3. Dipartimento di Informatica, Università di Pisa, Via Buonarroti 2, 56127, Italy

    Alberto Lluch-Lafuente

Authors
  1. Stefan Edelkamp
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Stefan Leue
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Alberto Lluch-Lafuente
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Stefan Edelkamp.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Edelkamp, S., Leue, S. & Lluch-Lafuente, A. Partial-order reduction and trail improvement in directed model checking. Int J Softw Tools Technol Transfer 6, 277–301 (2004). https://doi.org/10.1007/s10009-004-0151-z

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10009-004-0151-z

Keywords

Search

Navigation