Abstract
Given a white-box component C with specified unsafe states, we address the problem of automatically generating an interface that captures safe orderings of invocations of C's public methods. Method calls in the generated interface are guarded by constraints on their parameters. Unlike previous work, these constraints are generated automatically through an iterative refinement process. Our technique, named PSYCO (Predicate-based SYmbolic COmpositional reasoning), employs a novel combination of the L* automata learning algorithm with symbolic execution. The generated interfaces are three-valued, capturing whether a sequence of method invocations is safe, unsafe, or its effect on the component state is unresolved by the symbolic execution engine. We have implemented PSYCO as a new prototype tool in the JPF open-source software model checking platform, and we have successfully applied it to several examples.
Citation
Dimitra Giannakopoulou,
Zvonimir Rakamaric,
Vishwanath Raman
Symbolic Learning of Component Interfaces
Proceedings of the 19th International Static Analysis Symposium (SAS), 7460: 248--264, doi:10.1007/978-3-642-33125-1_18, 2012.
BibTeX
@inproceedings{2012_sas_grr,
title = {Symbolic Learning of Component Interfaces},
author = {Dimitra Giannakopoulou and Zvonimir Rakamaric and Vishwanath Raman},
booktitle = {Proceedings of the 19th International Static Analysis Symposium (SAS)},
series = {Lecture Notes in Computer Science},
volume = {7460},
publisher = {Springer},
editor = {Antoine Min\'e and David Schmidt},
pages = {248--264},
doi = {10.1007/978-3-642-33125-1_18},
year = {2012}
}
Acknowledgements
This research was supported by the NASA CMU grant NNA10DE60C. We would like to thank Peter Mehlitz for his help with Java PathFinder and Neha Rungta for reviewing a version of this paper.