Formal Verification of Protocol Properties of Sequential Java Programs

Protocol properties are essential properties in reusable library classes and object-oriented application frameworks. A protocol is the order in which the methods exported by the module have to be called, which can be referred as a set of allowed method call sequences. Checking protocol properties can be done at runtime, however, such runtime checks needs to insert checking codes into the source program, which results in decreasing the efficiency of the execution of the source program. In this paper an approach to formal verification of protocol properties of sequential Java programs is presented. At first protocol properties for a sequential Java program are specified as a set of finite state automata, where each finite state automaton represents a protocol for a class in the Java program. Then a set of rules are introduced for automatically generating all possible method call sequences of a Java program. These rules are established on different syntactic structures of Java programs. By applying these rules to a Java program, a context free grammar (CFG) will be produced for representing all possible method call sequences. These rules are given by a transforming function. Finally verification of protocol properties for a Java program is formalized by properly inserting actions of checking protocol properties in its method call sequences CFG. Protocol properties verifier can be build as the implementation of the method call sequences CFG with semantic actions. Some issues on our approach are discussed. The main contribution of our work is to use context free grammar to represent all the possible method call sequences of a Java program, which allows verifying protocol properties by inserting protocol checking into the implementation of CFG. Our approach separates protocol specifications from source code and makes no changes to the source code; therefore, it is more effective than runtime checking. Our work is useful for checking the correctness of a Java program with - - respect to its specification.