© University of Kent - Contact | Feedback | Legal | FOI | Cookies
Efficient detection of errors in java components using random environment and restarts
Pavel Parizek and Tomas Kalibera
In Proceedings of the 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 182-196. Springer, March 2010 [doi].Abstract
Software model checkers are being used mostly to discover specific types of errors in the code, since exhaustive verification of complex programs is not possible due to state explosion. Moreover, typical model checkers cannot be directly applied to isolated components such as libraries or individual classes. A common solution is to create an abstract environment for a component to be checked. When no constraints on component's usage are defined by its developers, a natural choice is to use a universal environment that performs all possible sequences of calls of component's methods in several concurrently-running threads. However, model checking of components with a universal environment is prone to state explosion.
In this paper we present a method that allows to discover at least some concurrency errors in component's code in reasonable time. The key ideas of our method are (i) use of an abstract environment that performs a random sequence of method calls in each thread, and (ii) restarts of the error detection process according to a specific strategy. We have implemented the method in the context of Java components and the Java PathFinder model checker. We have performed experiments on non-trivial Java components to show that our approach is viable.
Download publication 165 kbytes (PDF)Bibtex Record
@inproceedings{3126,
author = {Pavel Parizek and Tomas Kalibera},
title = {Efficient Detection of Errors in Java Components Using Random Environment and Restarts},
month = {March},
year = {2010},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {10.1007/978-3-642-12002-2_37},
url = {http://www.cs.kent.ac.uk/pubs/2010/3126},
publication_type = {inproceedings},
submission_id = {6907_1308766670},
ISBN = {978-3-642-12001-5},
booktitle = {Proceedings of the 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)},
publisher = {Springer},
refereed = {yes},
}