Interface Grammars for Modular Software Model Checking

Verification techniques relying on state enumeration (e.g., model checking) face two important challenges: the state-space explosion, an exponential increase in the state space as the number of components increases; and environment generation, modeling components that are either not available for analysis, or that cannot be handled by the verification tool in use. We propose a semi-automated approach for attacking these problems. In our approach, interfaces for the components not under analysis are specified using a specification language based on grammars. Specifically, an interface grammar for a component specifies the sequences of method invocations that are allowed by that component. We have built an compiler that takes the interface grammar for a component as input and generates a stub for that component. The stub thus generated can be used to replace that component during state space exploration, either to moderate state space explosion, or to provide an executable environment for the component under verification. We conducted a case study by writing an interface grammar for the Enterprise JavaBeans (EJB) persistence interface, and using the resulting stub to check EJB clients using the JPF model checker. Our results show that EJB clients can be verified efficiently with JPF using our approach.