The IMCOS Project
Incomplete Model Checking for Concurrent Object-Oriented
Systems
DFG Grant No.: LE 1342/1 - 2
Project Overview
Publications
Tools
people
IBOC
aLive
PONES
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.
People
There are still open positions in the IMCOS project. Welcome to join us.
Current Members and Participants
- Prof. Dr. Stefan Leue (homepage, DBLP entry)
- Wei Wei (homepage)
- Giorgos Giannakaras
- Sen Yang
- Dogan Saglem