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.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Adamek, J., Bures, T., Jezek, P., Kofron, J., Mencl, V., Parizek, P., Plasil, F.: Component Reliability Extensions for Fractal Component Model (2006), http://kraken.cs.cas.cz/ft/public/public_index.phtml
Atig, M.F., Bouajjani, A., Qadeer, S.: Context-Bounded Analysis for Concurrent Programs with Dynamic Creation of Threads. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505. Springer, Heidelberg (2009)
Biere, A.: PicoSAT Essentials. Journal on Satisfiability, Boolean Modeling and Computation (JSAT) 4 (2008)
Een, N., Sorensson, N.: An Extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)
Gomes, C.P., Selman, B., Kautz, H.A.: Boosting Combinatorial Search Through Randomization. In: Proceedings of AAAI 1998 (1998)
Groce, A., Visser, W.: Heuristics for Model Checking Java Programs. International Journal on Software Tools for Technology Transfer 6(4) (2004)
Havelund, K.: Using Runtime Analysis to Guide Model Checking of Java Programs. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885. Springer, Heidelberg (2000)
Huang, J.: The Effect of Restarts on the Efficiency of Clause Learning. In: Proceedings of the 20th International Joint Conference on Artificial Intelligence, IJCAI (2007)
Kautz, H., Horvitz, E., Ruan, Y., Gomes, C., Selman, B.: Dynamic Restart Policies. In: Proceedings of the 18th National Conference on Artificial Intelligence (AAAI 2002). AAAI Press, Menlo Park (2002)
Lu, S., Park, S., Seo, E., Zhou, Y.: Learning from Mistakes: A Comprehensive Study on Real World Concurrency Bug Characteristics. In: Proceedings of the 13th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS 2008). ACM, New York (2008)
Luby, M., Ertel, W.: Optimal Parallelization of Las Vegas Algorithms. In: Enjalbert, P., Mayr, E.W., Wagner, K.W. (eds.) STACS 1994. LNCS, vol. 775. Springer, Heidelberg (1994)
Luby, M., Sinclair, A., Zuckerman, D.: Optimal Speedup of Las Vegas Algorithms. Information Processing Letters 47(4) (1993)
van Moorsel, A.P.A., Wolter, K.: Analysis of Restart Mechanisms in Software Systems. IEEE Transactions on Software Engineering 32(8) (2006)
Parizek, P., Adamek, J., Kalibera, T.: Automated Construction of Reasonable Environment for Java Components. To appear in Proceedings of International Workshop on Formal Foundations of Embedded Software and Component-Based Software Architectures (FESCA 2009). ENTCS (2009)
Parizek, P., Plasil, F.: Specification and Generation of Environment for Model Checking of Software Components. In: Proceedings of International Workshop on Formal Foundations of Embedded Software and Component-Based Software Architectures (FESCA 2006). ENTCS, vol. 176(2) (2007)
Qadeer, S., Rehof, J.: Context-Bounded Model Checking of Concurrent Software. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 93–107. Springer, Heidelberg (2005)
Visser, W., Havelund, K., Brat, G., Park, S., Lerda, F.: Model Checking Programs. Automated Software Engineering Journal 10(2) (2003)
Walsh, T.: Search in a Small World. In: Proceedings of the 16th International Joint Conference on Artificial Intelligence, IJCAI 1999 (1999)
Apache Commons Pool, http://commons.apache.org/pool/
GNU Classpath, http://www.gnu.org/software/classpath/
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Parizek, P., Kalibera, T. (2010). Efficient Detection of Errors in Java Components Using Random Environment and Restarts. In: Esparza, J., Majumdar, R. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2010. Lecture Notes in Computer Science, vol 6015. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-12002-2_37
Download citation
DOI: https://doi.org/10.1007/978-3-642-12002-2_37
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-12001-5
Online ISBN: 978-3-642-12002-2
eBook Packages: Computer ScienceComputer Science (R0)