Automatic extraction of object-oriented component interfaces

ABSTRACT

Component-based software design is a popular and effective approach to designing large systems. While components typically have well-defined interfaces, sequencing information---which calls must come in which order---is often not formally specified.This paper proposes using multiple finite statemachine (FSM) submodels to model the interface of a class. A submodel includes a subset of methods that, for example, implement a Java interface, or access some particular field. Each state-modifying method is represented as a state in the FSM, and transitions of the FSMs represent allow able pairs of consecutive methods. In addition, state-preserving methods are constrained to execute only under certain states.We have designed and implemented a system that includes static analyses to deduce illegal call sequences in a program, dynamic instrumentation techniques to extract models from execution runs, and a dynamic model checker that ensures that the code conforms to the model. Extracted models can serve as documentation; they can serve as constraints to be enforced by a static checker; they can be studied directly by developers to determine if the program is exhibiting unexpected behavior; or they can be used to determine the completeness of a test suite.Our system has been run on several large code bases, including the joeq virtual machine, the basic Java libraries, and the Java 2 Enterprise Edition library code. Our experience suggests that this approach yields useful information.

REFERENCES

• 1: Glenn Ammons , Rastislav Bodík , James R. Larus, Mining specifications, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.4-16, January 16-18, 2002, Portland, Oregon
• 2: Thomas Ball , Sriram K. Rajamani, Automatically validating temporal safety properties of interfaces, Proceedings of the 8th international SPIN workshop on Model checking of software, p.103-122, May 2001, Toronto, Ontario, Canada
• 3: William R. Bush , Jonathan D. Pincus , David J. Sielaff, A static analyzer for finding dynamic programming errors, Software—Practice & Experience, v.30 n.7, p.775-802, June 2000 [doi>10.1002/(SICI)1097-024X(200006)30:7<775::AID-SPE309>3.0.CO;2-H]
• 4: A. N. Habermann R. H. Campbell. The specification of process synchronization by path expressions. Lecture Notes on Computer Science, 16, 1974.
• 5: Andy Chou , Benjamin Chelf , Dawson Engler , Mark Heinrich, Using meta-level compilation to check FLASH protocol code, Proceedings of the ninth international conference on Architectural support for programming languages and operating systems, p.59-70, November 2000, Cambridge, Massachusetts, United States
• 6: M. Dahm. Byte code engineering library. http://bcel.sourceforge.net, 2000.
• 7: Robert DeLine , Manuel Fähndrich, Enforcing high-level protocols in low-level software, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.59-69, June 2001, Snowbird, Utah, United States
• 8: D. Engler, B. Chelf, A. Chou, and S. Hallem. Checking system rules using system-specific, programmer-written compiler extensions. In Proceedings of the Symposium on Operating Systems Design and Implementation, pages 1-16, 2000.
• 9: Michael D. Ernst , Jake Cockrell , William G. Griswold , David Notkin, Dynamically discovering likely program invariants to support program evolution, Proceedings of the 21st international conference on Software engineering, p.213-224, May 16-22, 1999, Los Angeles, California, United States [doi>10.1145/302405.302467]
• 10: Jeanne Ferrante , Karl J. Ottenstein , Joe D. Warren, The program dependence graph and its use in optimization, ACM Transactions on Programming Languages and Systems (TOPLAS), v.9 n.3, p.319-349, July 1987 [doi>10.1145/24039.24041]
• 11: Jean-Yves Girard, Linear logic, Theoretical Computer Science, v.50 n.1, p.1-102, Jan. 30, 1987 [doi>10.1016/0304-3975(87)90045-4]
• 12: Georg Gottlob , Michael Schrefl , Brigitte Röck, Extending object-oriented systems with roles, ACM Transactions on Information Systems (TOIS), v.14 n.3, p.268-296, July 1996 [doi>10.1145/230538.230540]
• 13: Sudheendra Hangal , Monica S. Lam, Tracking down software bugs using automatic anomaly detection, Proceedings of the 24th International Conference on Software Engineering, May 19-25, 2002, Orlando, Florida [doi>10.1145/581339.581377]
• 14: M. Van Hilst and D. Notkin. Using C++ templates to implement role-based designs. Technical Report TR 95-07-02, Department of Computer Science and Engineering, University of Washington, 1996.
• 15: Viktor Kuncak , Patrick Lam , Martin Rinard, Role analysis, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.17-32, January 16-18, 2002, Portland, Oregon
• 16: David Lie , Andy Chou , Dawson Engler , David L. Dill, A simple method for extracting models for protocol code, Proceedings of the 28th annual international symposium on Computer architecture, p.192-203, June 30-July 04, 2001, Göteborg, Sweden
• 17: J. M. Lucassen , D. K. Gifford, Polymorphic effect systems, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.47-57, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73564]
• 18: Sun Microsystems. Java 2 platform, enterprise edition. http://java.sun.com/j2ee/, 2001.
• 19: Sun Microsystems. Petstore application for the java 2 platform, enterprise edition. http://java.sun.com/features/2001/05/petstore.html, 2001.
• 20: J. Nimmer and M. Ernst. Static verification of dynamically detected program invariants: Integrating Daikon and ESC/Java. In Electronic Notes in Theoretical Computer Science, volume 55, 2001.
• 21: Steven P. Reiss , Manos Renieris, Encoding program executions, Proceedings of the 23rd International Conference on Software Engineering, p.221-230, May 12-19, 2001, Toronto, Ontario, Canada
• 22: R. E. Strom , D. M. Yellin, Extending Typestate Checking Using Conditional Liveness Analysis, IEEE Transactions on Software Engineering, v.19 n.5, p.478-485, May 1993 [doi>10.1109/32.232013]
• 23: R E Strom , S Yemini, Typestate: A programming language concept for enhancing software reliability, IEEE Transactions on Software Engineering, v.12 n.1, p.157-171, Jan. 1986
• 24: P. Wadler. Linear types can change the world. In M. Broy and C. B. Jones, editors, IFIP TC 2 Working Conference on Programming Concepts and Methods, pages 561-581, 1990.
• 25: J. Whaley. The joeq virtual machine. http://sourceforge.net/projects/joeq, 2001.
• 26: R. Wiebicke. Linkverify. http://rw7.de/ralf/htmltools/index.en.html, 1998.
• 27: Zhichen Xu , Thomas W. Reps , Barton P. Miller, Typestate Checking of Machine Code, Proceedings of the 10th European Symposium on Programming Languages and Systems, p.335-351, April 02-06, 2001