Directed Model Checking

This project is joint work with Dr. Stefan Edelkamp and Dr. Alberto Lluch-Lafuente.

We investigate the use of directed, heuristics guided search algorithms in explicit state model checking. The use of directed search algorithms decreases the number of expanded states when searching for safety property violations or when searching for acceptance cycles in liveness property analysis. At the same time, the error trails generated by the model checker are shorter and hence more easily comprehensible. So far we have applied this idea to Promela, which is the input language of the SPIN model checker. We validated safety properties (assertions, deadlock detection, invariants) and general temporal properties specified in LTL using the experimental HSF-SPIN workbench using a variety of communication protocols, including real-world protocols like the CORBA GIOP protocol.

Publications

  • Dragan Bosnacki, Stefan Leue and Alberto Lluch Lafuente: Partial-order reduction for general state exploring algorithms , Volume 11, Pages 39-51, International Journal on Software Tools for Technology Transfer (STTT), Springer Berlin / Heidelberg, DOI: 10.1007/s10009-008-0093-y, 2009. (PDF)
  • Dragan Bosnacki, Stefan Leue, and Alberto Lluch Lafuente: Partial-Order Reduction for General State Exploring Algorithms, To appear in: International Journal on Software Tools for Technology Transfer, 2007. (PDF)
  • Dragan Bosnacki, Stefan Leue, and Alberto Lluch Lafuente: Partial-Order Reduction for General State Exploring Algorithms, Pages 271-287, Proceedings of the 13th International SPIN Workshop on Model Checking of Software, LNCS 3925, Lecture Notes in Computer Science, Springer Verlag, 2006. (PDF)
  • Dragan Bosnacki, Stefan Leue, and Alberto Lluch Lafuente: Partial-Order Reduction for General State Exploring Algorithms, Technical Report soft-05-02, Chair for Software Engineering, University of Konstanz, 2005. (PDF)
  • Jianbin Tan, George S. Avrunin, Lori A. Clarke, Shlomo Zilberstein, and Stefan Leue: Heuristic-Guided Counterexample Search in FLAVERS, Pages 201-210, Proceedings of the 12th ACM Symposium on the Foundations of Software Engineering, ACM Press, 2004. (PDF)
  • Stefan Edelkamp, Stefan Leue, and Alberto Lluch-Lafuente: Partial-Order Reduction and Trail Improvement in Directed Model Checking, Pages 277-301, International Journal on Software Tools for Technology Transfer 6 (4), Springer Verlag, 2004. (PDF)
  • tefan Edelkamp, Stefan Leue, and Alberto Lluch-Lafuente: Directed Explicit-State Model Checking in the Validation of Communication Protocols, Pages 247-267, International Journal on Software Tools for Technology Transfer 5 (2-3), Springer Verlag, 2004. (PDF)
  • Alberto Lluch-Lafuente, Stefan Edelkamp, Stefan Leue: Partial Order Reduction in Directed Model Checking, Volume 2318, Pages 112-127, Proceedings of the 9th International SPIN Workshop on Software Model Checking, Lecture Notes in Computer Science, Springer Verlag, 2002. (PDF)
  • Stefan Edelkamp, Alberto Lluch Lafuente and Stefan Leue: Protocol Verification with Heuristic Search, Pages 75-83, Proceedings of the AAAI-Spring Symposium on Model-based Validation of Intelligence, Stanford University, 2001. (PDF)
  • Stefan Edelkamp, Alberto Lluch Lafuente, Stefan Leue: Directed Explicit Model Checking with HSF-SPIN, Pages 57-79, Proceedings of 8th International SPIN Workshop on Model Checking Software, LNCS 2057, Lecture Notes in Computer Science, Springer Verlag, 2001. (PDF)
  • Stefan Edelkamp, Alberto Luch Lafuente and Stefan Leue: Trail-Directed Model Checking, Pages 343-356, Proceedings of the Workshop on Software Model Checking, Electrical Notes in Theoretical Computer Science 55 (3), Elsevier, 2001. (PDF)
  • Stefan Edelkamp, Stefan Leue, Alberto Lluch-Lafuente: Partial Order Reduction in Directed Model Checking, Technical Report No. 162, Institute for Computer Science, Albert-Ludwigs-University Freiburg, 2001. (PDF)
  • Stefan Edelkamp, Stefan Leue, Alberto Lluch-Lafuente: Directed Explicit-State Model Checking in the Validation of Communication Protocols, Technical Report No. 161, Institute for Computer Science, Albert-Ludwigs-University Freiburg, 2001. (PDF)