Enriching Java Enterprise interfaces with formal sequential contracts

ABSTRACT

Many software systems are stateful or have stateful components, i.e. they manage and process data depending on certain steps performed before. For this reason, sequential contracts are of interest that describe component interfaces with respect to sequences of invocations leaving the component in a valid state. While sophisticated models for this purpose exist, component frameworks don't support sequential contracts, so that a validation of the state is performed algorithmically and mixed-up with application logic in method contents. In this contribution we present (1) meta data for object-oriented program code that allow to annotate component interfaces with sequential contracts and (2) a pattern and tools integrating sequential contracts in Java Enterprise components. The contracts can then be modeled as part of the program code at development time and be interpreted at run time to prevent invalid method invocations and provide tracing data in case of errors.

References

1. Plasil, F., Visnovsky, S.: Behavior Protocols for Software Components. IEEE Transactions on Software Engineering (2002) 1056--1076
2. Sun Microsystems, Inc.: JSR 316: Java#8482;Platform, Enterprise Edition 6 (Java EE 6) Specification (December 2009) http://jcp.org/en/jsr/detail?id=316.
3. Sun Microsystems, Inc.: Introduction to the Java#8482; EE 6 Platform. White Paper (2009)
4. de Alfaro, L., Henzinger, T. A.: Interface Automata. In: Proceedings of the Ninth Annual Symposium on Foundations of Software Engineering (FSE), ACM. (2001) 109--120
5. Sun Microsystems, Inc.: JSR 175: A Metadata Facility for the Java#8482;Programming Language (2004) http://jcp.org/en/jsr/detail?id=175.
6. Cheon, Y., Perumandla, A.: Specifying and Checking Method Call Sequences of Java Programs. Software Quality Journal 15(1) (March 2007) 7--25
7. Leavens, G., Cheon, Y.: Design by Contract with JML. http://www.jmlspecs.org/jmldbc.pdf (2006)
8. Heinlein, C.: Advanced Thread Synchronization in Java Using Interaction Expressions. Objects, Components, Architectures, Services, and Applications for a Networked World 2591/2009 (2009) 345--365
9. Pavel, S., Noye, J., Poizat, P., Royer, J. C.: Java Implementation of a Component Model with Explicit Symbolic Protocols. In: In Proceedings of the 4th International Workshop on Software Composition (SC'05), volume 3628 of LNCS, Springer-Verlag (2005) 115--124
10. Farías, A., Guéhéneuc, Y., Südholt, M.: Integrating Behavioral Protocols in Enterprise Java Beans. In: 11th OOPSLA Workshop on Behavioral Semantics: Serving the Customer. OOPSLA '02, New York, NY, USA, ACM (2002) 76--77
11. Reussner, R., Becker, S., Happe, J., Koziolek, H., Krogmann, K., Kuperberg, M.: The Palladio Component Model. Technical report, Chair for Software Design & Quality (SDQ), University of Karlsruhe (TH), Germany (May 2007)
12. Beugnard, A., Jézéquel, J. M., Plouzeau, N., Watkins, D.: Making Components Contract Aware. Computer 32(7) (1999) 38--45
13. Object Management Group: Common Object Request Broker Architecture (CORBA) Specification, Version 3.1, Part 1: CORBA Interfaces. Technical report, Object Management Group (January 2008) http://www.omg.org/spec/CORBA/3.1/Interfaces/PDF/.
14. Demers, F. N., Malenfant, J.: Reflection in logic, functional and object-oriented programming: A Short Comparative Study. In: In IJCAI '95 Workshop on Reflection and Metalevel Architectures and their Applications in AI. (1995) 29--38
15. Lynch, N. A., Tuttle, M. R.: Hierarchical Correctness Proofs for Distributed Algorithms. In: Proceedings of the sixth annual ACM Symposium on Principles of distributed computing. PODC '87, New York, NY, USA, ACM (1987) 137--151
16. Larsen, K. G., Pettersson, P., Yi, W.: Uppaal in a Nutshell. Int. Journal on Software Tools for Technology Transfer 1(1--2) (Oct 1997) 134--152
17. Wasylkowski, A., Zeller, A., Lindig, C.: Detecting Object Usage Anomalies. In: Proceedings of the 6th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering. ESEC-FSE '07, New York, NY, USA, ACM (2007) 35--44
18. The Eclipse Foundation: Eclipse website http://www.eclipse.org/.
19. Kiczales, G., Lamping, J., Mendhekar, A., Maeda, C., Lopes, C., Loingtier, J. M., Irwing, J.: Aspect-Oriented Programming. ECOOP '97 - Object-Oriented Programming: 11th European Conference LNCS 1241 (1997) 220--242
20. Sun Microsystems: Dynamic Proxy Classes, Java SE Documentation (January 2010) http://java.sun.com/javase/6/docs/technotes/guides/reflection/proxy.html.

Index Terms

• General and reference

  • Cross-computing tools and techniques

    • Verification

• Software and its engineering

  • Software creation and management

    • Software development process management

    • Software verification and validation

      • Formal software verification

  • Software notations and tools

    • General programming languages

      • Language features

        • Modules / packages

      • Language types

  • Software organization and properties

    • Software functional properties

      • Formal methods

        • Software verification

• Theory of computation

  • Semantics and reasoning

    • Program reasoning

      • Program verification