Interface Grammars for Modular Software Model Checking.

Verification techniques that rely on state enumeration (such as model checking) face two important challenges: 1) state space explosion: exponential increase in the state space with the increasing number of components and 2) environment generation: modeling components that are either not available for analysis or that are outside the scope of the verification tool at hand. We propose a semiautomated approach for attacking these two problems. In our approach, interfaces for the components that are outside the scope of the current verification effort are specified using an interface specification language based on grammars. Specifically, an interface grammar for a component specifies the sequences of method invocations that are allowed by that component. Using interface grammars, one can specify nested call sequences that cannot be specified using interface specification formalisms that rely on finite state machines. Moreover, our interface grammars allow specification of semantic predicates and actions, which are Java code segments that can be used to express additional interface constraints. We have built an interface compiler that takes the interface grammar for a component as input and generates a stub for that component. The resulting stub is a table-driven parser. Invocation of a method within the component becomes the look-ahead symbol for the stub/parser. The stub/parser uses a parser stack, the look- ahead, and a parse table to guide the parsing. The semantic predicates and semantic actions that appear on the right-hand side of the production rules are executed when they appear at the top of the stack. The stub/parser generated from the interface grammar of a component can be used to replace that component during state space exploration, either to assuage the state space explosion or to provide an executable environment for the component that is being verified. We conducted a case study by writing an interface grammar for the Enterprise JavaBeans (EJB) persistence interface. Using our interface compiler, we automatically generated an EJB stub using the EJB interface grammar. We used the JPF model checker to check EJB clients using this automatically generated EJB stub. Our results show that EJB clients can be verified efficiently with JPF using our approach, whereas they cannot be verified with JPF directly since JPF cannot handle EJB components. [ABSTRACT FROM AUTHOR]