The IMCOS Project
Incomplete Model Checking for Concurrent Object-Oriented Systems

DFG Grant No.: LE 1342/1 - 2

Project Overview

The project aims at developing incomplete but scalable and fully automated methods for the analysis and verification of concurrent, object-oriented software systems.

Concurrent object-oriented systems are complex systems that usually consist of a large number of autonomously running components. The components of a system may communicate with each other by exchanging messages asynchronously over computer networks. The message buffers used to store unprocessed messages may have unbounded capacities. Such a system may possess a huge or even infinite global state space that impedes the application of traditional state enumeration based verification approaches such as model checking.

Precursory Work

In our precursory work, we have implemented an efficient but incomplete verification framework based on Integer Linear Program (ILP) solving. The framework concentrates on the analysis of the local behavior of each system component. In this way it avoids the consideration of the potentially exponentially many interleavings of the executions of each individual component. The framework makes use of a series of conservative abstraction steps, tailored to each concrete property being checked, to transform an original system into a set of control flow cycles that over-approximates the behavior of the original system. A necessary condition for the violation of the property is then given on the message passing effects of the cycles, and further encoded into a homogeneous ILP problem that can be solved in polynomial time. The solution space of the ILP problem represents the property violating behavior, and its infeasibility implies therefore the satisfaction of the property. The framework is inevitably incomplete because the property checking problems that we consider are undecidable. On the other hand, the conservative abstractions that the framework employs also contribute imprecision to the analysis. In order to address this problem, we have developed counterexample-guided abstraction refinement techniques centered around the discovery of cycle dependencies. Within the above mentioned framework we have designed verification methods for the two important properties: buffer boundedness and livelock freedom.

The buffer boundedness and livelock freedom tests have been applied to the verification of UML RT and Promela models, thanks to the code abstraction techniques that we have developed individually for the two widely used modeling languages. In particular, we have implemented an automated termination proving method for program loops, which does not rely on the explicit construction of ranking functions.

The work described above has been published in several papers (see the publications section). Prototype tools were also built to evaluate the property checking methods, with which we obtained promising results on real life system models.

Future Work

There are several directions that we will follow to proceed with the IMCOS project.

Extending the ILP-based verification framework. One goal is to generalize the framework to deal with more concrete properties such as deadlock freedom. Unlike buffer boundedness and livelock freedom, deadlock freedom is not a property concerning infinite executions. Therefore, it cannot be checked solely by the analysis of control flow cycles. One possible solution is to combine our cycle analysis with the state equation based ILP verification approach proposed by Avrunin and Corbett.

Improving abstractions and refinements. The precision and the full automation of the verification methods rely heavily on the use of both efficient and effective automatic abstraction and refinement techniques. For the improvement of the current abstraction and refinement techniques, we resort to developing static analysis methods that retrieve useful information of the runtime behavior of models at compile time. In particular, we will improve the previous work on termination proofs and cycle dependency discovery, for they stand at the heart of automating the abstraction of UML RT transition action code, and the refinement procedure, respectively.

Developing debugging methods. The current framework can only prove that a counterexample is spurious, i.e., it does not correspond to any real executions of the original model. However, when a counterexample that we found is indeed a real property violating scenario, we need to replay it in the original model for the debugging of the model. More precisely, we need to find an execution of the model that the counterexample corresponds to. For this purpose, we aim to use the so-called directed model checking, based on heuristic searching, to search for a property violating execution in the vast or even infinite state space of the original model. The idea is to use the information provided in the counterexample to derive effective heuristics to guide the search in the global state space.

Publications

  • S. Leue, A. Stefanescu and W. Wei. A livelock freedom analysis for infinite state asynchronous reactive systems. In Proc. of CONCUR 2006, LNCS 4137, pages 79--94. Springer, 2006. (bibtex, pdf)
  • S. Leue and W. Wei. A region graph based approach to termination proofs. In Proc. of TACAS 2006, LNCS 3920, pages 318--333. Springer, 2006. (bibtex, pdf)
  • S. Leue and W. Wei. Counterexample-based refinement for a boundedness test for CFSM languages. In Proc. of SPIN 2005, LNCS 3639, pages 58--74. Springer, 2005. (bibtex, pdf)
  • S. Leue, R. Mayr and W. Wei. A scalable incomplete test for message buffer overflow in Promela models. In Proc. of SPIN 2004, LNCS 2989, pages 216--233. Springer, 2004. (bibtex, pdf)
  • S. Leue, R. Mayr and W. Wei. A scalable incomplete test for the boundedness of UML RT models. In Proc. of TACAS 2004, LNCS 2988, pages 327--341. Springer, 2004. (bibtex, pdf)

Tools

IBOC is a buffer boundedness checker for Rational Rose Real Time models and Promela models. It is written in Visual C++ and uses an open source LP solver named "lp_solve". More details of the theory behind the tool and its current status can be found here.

aLive is a livelock freedom checker for Promela models, written in Visual C++ and using also "lp_solve". More details can be found here.

PONES is a termination prover for program loops. It is written in Java. More details can be found here.

Current Members and Participants

  • Prof. Dr. Stefan Leue (homepage, DBLP entry)
  • Wei Wei
  • Giorgos Giannakaras
  • Sen Yang
  • Dogan Saglem

Former Members and Participants

Publications

  • Stefan Leue and Wei Wei: Integer Linear Programming Based Property Checking for Asynchronous Reactive Systems, IEEE Transactions on Software Engineering, vol. 99, 2011. (PDF)
  • Matthias Kuntz, Stefan Leue and Christoph Scheben: Extending Non-Termination Proof Techniques to Asynchronously Communicating Concurrent Programs, Third International Workshop on Invariant Generation (WING 2010), 2010. (PDF)
  • Matthias Kuntz, Stefan Leue, Christoph Scheben, Wei Wei, Sen Yang: Heuristic Search for Unbounded Executions, Technical Report soft-09-02, Chair for Software Engineering, University of Konstanz, 2009. (PDF)
  • hristian Dax, Felix Klaedtke and Stefan Leue: Specification Languages for Stutter-Invariant Regular Properties, In Proceedings of Automated Technology for Verification and Analysis, 7th International Symposium, ATVA 2009, Lecture Notes in Computer Science, Springer Verlag, 2009. (PDF)
  • Bahareh Badban, Wan Fokkink, Jaco van de Pol: Mechanical Verification of a Two-Way Sliding Window Protocol, Communicating Process Architectures (CPA) conference, 2008. (PDF)
  • Wei Wei: Incomplete Property Checking for Asynchronous Reactive Systems, Doctoral Dissertation, University of Konstanz, 2008. (PDF)
  • Stefan Leue, Alin Stefanescu and Wei Wei: Dependency Analysis for Control Flow Cycles in Reactive Communicating Processes, Pages 176-195, Proceedings of 15th International SPIN Workshop on Model Checking of Software (SPIN '08), Lecture Notes in Computer Science, Volume 5156. Springer Verlag., 2008. (PDF)
  • Stefan Leue, Alin Stefanescu and Wei Wei: An AsmL Semantics for Dynamic Structures and Run Time Schedulability in UML-RT, Pages 238-257, Proceedings of 46th International Conference on Objects, Models, Components, Patterns (TOOLS '08), Lecture Notes in Business and Information Processing, Volume 11. Springer Verlag., 2008. (PDF) (Long Version PDF)
  • Stefan Leue, Alin Stefanescu, and Wei Wei: A Livelock Freedom Analysis for Infinite State Asynchronous Reactive Systems, Pages 79-94, Proceedings of 17th International Conference on Concurrency Theory CONCUR '06, LNCS 4137, Lecture Notes in Computer Science, Springer Verlag., 2006. (PDF) (Long Version PDF)
  • Stefan Leue and Wei Wei: A Region Graph Based Approach to Termination Proofs, Technical Report soft-06-01, Chair for Software Engineering, University of Konstanz, 2006. (PDF)
  • Stefan Leue and Wei Wei: A Region Graph Based Approach to Termination Proofs, Pages 318-333, Proceedings of 12th. International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS '06, LNCS 3920, Lecture Notes in Computer Science, Springer Verlag, 2006. (PDF)
  • Stefan Leue and Wei Wei: Counterexample-based Refinement for a Boundedness Test for CFSM Languages, Pages 58-74,Proceedings of 12th International SPIN Workshop on Model Checking of Software SPIN2005, LNCS 3639, Lecture Notes in Computer Science, Springer Verlag, 2005. (PDF)
  • Stefan Leue and Wei Wei: Counterexample Refinement for a Boundedness Test for CFSM Languages, Technical Report soft-05-01, Chair for Software Engineering, University of Konstanz, 2005. (PDF)
  • Stefan Leue, Richard Mayr, and Wei Wei: A Scalable Incomplete Test for Message Buffer Overflow in Promela Models, Pages 216-233, Proceedings of the 11th International SPIN Workshop on Model Checking Software SPIN 2004, LNCS 2989, Lecture Notes in Computer Science, Springer Verlag, 2004. (PDF)
  • Stefan Leue, Richard Mayr, and Wei Wei: A Scalable Incomplete Test for the Boundedness of UML RT Models, Pages 327-341,Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS 2004, LNCS 2988, Lecture Notes in Computer Science, Springer Verlag, 2004. (PDF)