Contemporary software development emphasizes components with clearly specified APIs. In current practice, while a typical software component has a precise (static) interface in terms of methods it supports, the information about the correct sequencing of method calls is missing. Behavioral interfaces can capture such temporal constraints, and can play a critical role in documentation, maintenance, testing, and compositional analysis. This proposal is centered around specification and automatic extraction of such interfaces. Research will be pursued to develop formal notions of behavioral interfaces for Java classes and web services; algorithms for automatic synthesis of interfaces using abstraction, learning, and symbolic model checking; application of interfaces for compositional software model checking via assume-guarantee reasoning; and experimentation and evaluation on Java2SDK library classes.
