Abstract
Partial order reduction is a very succesful technique for avoiding the state explosion problem that is inherent to explicit state model checking of asynchronous concurrent systems. It exploits the commutativity of concurrently executed transitions in interleaved system runs in order to reduce the size of the explored state space. Directed model checking on the other hand addresses the state explosion problem by using guided search techniques during state space exploration. As a consequence, shorter errors trails are found and less search effort is required than when using standard depth-first or breadth-first search. We analyze how to combine directed model checking with partial order reduction methods and give experimental results on how the combination of both techniques performs.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
R. Alur, R. Brayton, T. Henzinger, S. Qaderer, and S. Rajamani. Partial-order reduction in symbolic state space exploration. In Computer Aided Verification (CAV), Lecture Notes in Computer Science, pages 340–351. Springer, 1997.
C.-T. Chou and D. Peled. Formal verification of a partial-order reduction technique for model checking. In Tools and Algorithms for Construction and Analysis of Systems, pages 241–257, 1996.
E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. MIT Press, 1999.
J. M. Cobleigh, L. A. Clarke, and L. J. Osterweil. The right algorithm at the right time: Comparing data flow analysis algorithms for finite state verification. In Proceedings of the 23 rd ICSE, pages 37–46, 2001.
D. Dolev, M. Klawe, and M. Rodeh. An O(n log n) unidirectional distributed algorithm for extrema finding in a circle. Journal of Algorithms, 1982.
S. Edelkamp, A. L. Lafuente, and S. Leue. Trail-directed model checking. In S. D. Stoller and W. Visser, editors, Electronic Notes in Theoretical Computer Science, volume 55. Elsevier Science Publishers, 2001.
S. Edelkamp, A. Lluch-Lafuente, and S. Leue. Directed model-checking in HSFSPIN. In 8th International SPIN Workshop on Model Checking Software, Lecture Notes in Computer Science 2057, pages 57–79. Springer, 2001.
S. Edelkamp, A. Lluch-Lafuente, and S. Leue. Protocol verification with heuristic search. In AAAI-Spring Symposium on Model-based Validation of Intelligence, pages 75–83, 2001.
P. Godefroid. Using partial orders to improve automatic verification methods. In E. M. Clarke, editor, Proceedings of the 2nd International Conference on Computer-Aided Verification (CAV’ 90), Rutgers, New Jersey, 1990, number 531, pages 176–185, Berlin-Heidelberg-New York, 1991. Springer.
P. E. Hart, N. J. Nilsson, and B. Raphael. A formal basis for heuristic determination of minimum path cost. IEEE Transactions on on Systems Science and Cybernetics, 4:100–107, 1968.
G. Holzmann, P. Godefroid, and D. Pirottin. Coverage preserving reduction strategies for reachability analysis. In Proc. 12th Int. Conf on Protocol Specification, Testing, and Verification, INWG/IFIP, Orlando, Fl., June 1992.
G. J. Holzmann. Algorithms for automated protocol verification. AT&T Technical Journal, 69(2):32–44, Feb. 1990. Special Issue on Protocol Testing, Specification, and Verification.
M. Kamel and S. Leue. Formalization and validation of the General Inter-ORB Protocol (GIOP) using PROMELA and SPIN. International Journal on Software Tools for Technology Transfer, 2(4):394–409, 2000.
M. Kamel and S. Leue. VIP: A visual editor and compiler for v-Promela. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Lecture Notes in Computer Science, pages 471–486. Springer, 2000.
R. E. Korf. Depth-first iterative-deepening: An optimal admissible tree search. Artificial Intelligence, 27(1):97–109, 1985.
R. P. Kurshan, V. Levin, M. Minea, D. Peled, and H. Yenigun. Static partial order reduction. In Tools and Algorithms for Construction and Analysis of Systems, pages 345–357, 1998.
F. J. Lin, P. M. Chu, and M. Liu. Protocol verification using reachability analysis: the state space explosion problem and relief strategies. ACM, pages 126–135, 1988.
D. McVitie and L. Wilson. The stable marriage problem. Communications of the ACM, 14(7):486–492, 1971.
N. J. Nilsson. Principles of Artificial Intelligence. Tioga Publishing Co., Palo Alto, California, 1980.
J. Pearl. Heuristics. Addison-Wesley, 1985.
D. A. Peled. Combining partial order reductions with on-the-fly model-checking. Formal Methods in Systems Design, 8:39–64, 1996.
D. A. Peled. Ten years of partial order reduction. In Computer Aided Verification, number 1427 in Lecture Notes in Computer Science, pages 17–28. Springer, 1998.
A. Valmari. A stubborn attack on state explosion. Lecture Notes in Computer Science, 531:156–165, 1991.
C. H. Yang and D. L. Dill. Validation with guided search of the state space. In Conference on Design Automation (DAC), pages 599–604, 1998.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lluch-Lafuente, A., Edelkamp, S., Leue, S. (2002). Partial Order Reduction in Directed Model Checking. In: Bošnački, D., Leue, S. (eds) Model Checking Software. SPIN 2002. Lecture Notes in Computer Science, vol 2318. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46017-9_10
Download citation
DOI: https://doi.org/10.1007/3-540-46017-9_10
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43477-1
Online ISBN: 978-3-540-46017-6
eBook Packages: Springer Book Archive