Abstract

This paper addresses the problem of efficient generation of component interfaces through learning. Given a white-box component C with specified unsafe states, an interface captures safe orderings of invocations of C's public methods. In previous work we presented PSYCO, an interface generation framework that combines automata learning with symbolic component analysis: learning drives the framework in exploring different combinations of method invocations, and symbolic analysis computes method guards corresponding to constraints on the method parameters for safe execution. In this work we propose solutions to the two main bottlenecks of PSYCO. The explosion of method sequences that learning generates to validate its computed interfaces is reduced through partial order reduction resulting from a static analysis of the component. To avoid scalability issues associated with symbolic analysis, we propose novel algorithms that are primarily based on dynamic, concrete component execution, while resorting to symbolic analysis on a limited, as needed, basis. Dynamic execution enables the introduction of a concept of state matching, based on which our proposed approach detects, in some cases, that it has exhausted the exploration of all component behaviors. On the other hand, symbolic analysis is enhanced with symbolic summaries. Our new approach, X-PSYCO, has been implemented in the Java Pathfinder (JPF) software verification platform. We demonstrated the effectiveness of X-PSYCO on a number of realistic software components by generating more complete and precise interfaces than was previously possible.

Citation

BibTeX

@inproceedings{2013_issta_hgr,
  title = {Hybrid Learning: Interface Generation through Static, Dynamic, and Symbolic Analysis},
  author = {Falk Howar and Dimitra Giannakopoulou and Zvonimir Rakamaric},
  booktitle = {Proceedings of the International Symposium on Software Testing and Analysis (ISSTA)},
  publisher = {ACM},
  pages = {268--279},
  doi = {10.1145/2483760.2483783},
  year = {2013}
}

Acknowledgements

We would like to thank Vishwanath Raman for many fruitful discussions and his help with jpf-jdart, Peter Mehlitz for the suggested improvements concerning the integration with JPF, Oksana Tkachuk for providing support for the static analysis engine in OCSEGen, and Malte Isberner and Marko Dimjasevic for their helpful feedback. This research was partly sponsored by United States National Aeronautics and Space Administration (NASA) under Prime Contract No. NNA10DE60C.