2010 | OriginalPaper | Chapter
Learning Component Interfaces with May and Must Abstractions
Authors : Rishabh Singh, Dimitra Giannakopoulou, Corina Păsăreanu
Published in: Computer Aided Verification
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
Component interfaces are the essence of modular program analysis. In this work, a component interface documents correct sequences of invocations to the component’s public methods. We present an automated framework that extracts finite
safe
,
permissive
, and
minimal
interfaces, from potentially infinite software components. Our proposed framework uses the L* automata-learning algorithm to learn finite interfaces for an infinite-state component. It is based on the observation that an interface
permissive
with respect to the component’s must abstraction and
safe
with respect to its may abstraction provides a precise characterization of the legal invocations to the methods of the concrete component. The abstractions are refined automatically from counterexamples obtained during the reachability checks performed by our framework. The use of must abstractions enables us to avoid an exponentially expensive determinization step that is required when working with may abstractions only, and the use of L* guarantees minimality of the generated interface. We have implemented the algorithm in the ARMC tool and report on its application to a number of case studies including several Java2SDK and J2SEE library classes as well as to NASA flight-software components.