Access Restriction

Author Ying Jin
Source IEEE Xplore Digital Library
Content type Text
Publisher Institute of Electrical and Electronics Engineers, Inc. (IEEE)
File Format PDF
Copyright Year ©2007
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword Formal verification ♦ Protocols ♦ Java ♦ Runtime ♦ Automata ♦ Writing ♦ Program processors ♦ Information analysis ♦ Performance analysis ♦ Production
Abstract 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.
Description Author affiliation: Jilin Univ., Changchun (Ying Jin)
ISBN 0769528708
ISSN 07303157
Educational Role Student ♦ Teacher
Age Range above 22 year
Educational Use Research ♦ Reading
Education Level UG and PG
Learning Resource Type Article
Publisher Date 2007-07-24
Publisher Place China
Rights Holder Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Size (in Bytes) 238.10 kB
Page Count 8
Starting Page 475
Ending Page 482

Source: IEEE Xplore Digital Library