© University of Kent - Contact | Feedback | Legal | FOI | Cookies
Automated construction of reasonable environment for Java components
Pavel Parizek, Jiri Adamek, and Tomas Kalibera
In Proceedings of the 6th International Workshop on Formal Engineering Approaches to Software Components and Architectures (FESCA), volume 253 of Electronic Notes in Theoretical Computer Science, pages 182-196. Elsevier, March 2009 [doi].Abstract
In software component verification, one of the challenges is model checking of isolated components. The environment of an isolated component is unknown, and therefore a part of an input to a model checker is missing. This problem can be addressed via automated generation of an artificial environment -- component and its environment form a complete program that can be verified using common model checkers.
Focusing on concurrency errors in Java components, we propose to automatically generate a reasonable artificial environment that makes efficient detection of concurrency errors with Java PathFinder possible. Such an environment executes in parallel those component's methods that interact via concurrency constructs of Java and thus likely contain concurrency errors. We employ static code analysis to identify sets of methods to be executed in parallel and a metric to order the sets according to the degree of interaction. Benefits of the technique are illustrated on results of experiments performed on real-life Java components.
Download publication 239 kbytes (PDF)Bibtex Record
@inproceedings{3138,
author = {Pavel Parizek and Jiri Adamek and Tomas Kalibera},
title = {Automated Construction of Reasonable Environment for {Java} Components},
month = {March},
year = {2009},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {10.1016/j.entcs.2009.09.033},
url = {http://www.cs.kent.ac.uk/pubs/2009/3138},
publication_type = {inproceedings},
submission_id = {1089_1311973636},
booktitle = {Proceedings of the 6th International Workshop on Formal Engineering Approaches to Software Components and Architectures (FESCA)},
volume = {253},
number = {1},
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier},
refereed = {yes},
}