Interface Grammars for Modular Software Model Checking

We propose an interface specification language based on grammars for modular software model checking. In our interface specification language, component interfaces are specified as context free grammars. 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 generated from the input interface grammar. Invocation of a method within the component becomes the lookahead symbol for the stub/parser. The stub/parse...

• Type: Journal
• Year: 2008
• Where: TSE
• Authors: Graham Hughes, Tevfik Bultan
• Keywords: Grammar, Interface Grammar, Interface Specification, TSE 2008