Consistency of Java Transactions

  • Suad Alagić
  • Jeremy Logan
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2921)


A model of Java transactions is presented and the basic formal properties of this model with respect to behavioral compatibility and database integrity are proved. An implementation technique for incorporating constraints into the existing Java technology is developed, and a sophisticated theorem prover technology is integrated into this environment capable of enforcing behavioral compatibility and verifying transaction safety. The model of Java transactions developed in this paper is based on the subtle interplay of constraints, bounded parametric polymorphism and orthogonal persistence. The approach is based on a correct solution for extending Java with parametric polymorphism along with a technique for integrating logic-based constraints into Java class files and class objects. The Java Core Reflection is extended accordingly. The technique for enforcing database integrity constraints is based on the PVS theorem prover technology, and it combines static and dynamic checking to attain reasonable performance. The theorem prover technology is itself based on a sophisticated type system equipped with a form of semantic subtyping and parametric polymorphism. The higher-order features of this technology are proved to be critical in dealing with the problems of behavioral compatibility and transaction verification.


Class Object Integrity Constraint Java Virtual Machine Database Transaction Database Integrity 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Alagić, S., Kouznetsova, S.: Behavioral compatibility of self-typed theories. In: Magnusson, B. (ed.) ECOOP 2002. LNCS, vol. 2374, pp. 585–608. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  2. 2.
    Alagić, S.: Semantics of temporal classes. Information and Computation 163, 60–102 (2000)Google Scholar
  3. 3.
    Alagić, S., Ngyen, T.: Parametric polymorphism and orthogonal persistence. In: Proceedings of the ECOOP 2000 Symposium on Objects and Databases. Lecture Notes in Computer Science, vol. 1813, pp. 32–46 (2001)Google Scholar
  4. 4.
    Atkinson, M., Daynes, L., Jordan, M.J., Printezis, T., Spence, S.: An orthogonally persistent JavaTM. In: ACM SIGMOD Record, vol. 25, pp. 68–75. ACM, New York (1996)Google Scholar
  5. 5.
    Daynes, L.: Extensible transaction management in PJava. In: Morrison, R., Jordan, M., Atkinson, M. (eds.) Advances in Persistent Object Systems. Morgan Kaufmann Publishers, San Francisco (1999)Google Scholar
  6. 6.
    Daynes, L., Atkinson, M., Valduirez, P.: Efficient support for customized concurrency control in Persistent Java. In: Proceedings of the Int. Workshop on Advanced Transaction Models and Architecture (in conjunction with VLDB 1996), India (September 1996)Google Scholar
  7. 7.
    Benzaken, V., Doucet, D.: Themis: A database language handling integrity constraints. VLDB Journal 4, 493–517 (1994)CrossRefGoogle Scholar
  8. 8.
    Bretl, B., Otis, A., San Soucie, M., Schuchardt, B., Venkatesh, R.: Persistent Java objects in 3 tier architectures. In: Morrison, R., Jordan, M., Atkinson, M. (eds.) Advances in Persistent Object Systems, pp. 236–249. Morgan Kaufmann, San Francisco (1999)Google Scholar
  9. 9.
    Cattell, R.G.G., Barry, D., Berler, M., Eastman, J., Jordan, D., Russell, C., Schadow, O., Stanienda, T., Velez, F.: The Object Data Standard: ODMG 3.0. Morgan Kaufmann, San Francisco (2000)Google Scholar
  10. 10.
    Gehani, N., Jagadish, H.V.: Ode as active database: Constraints and triggers. In: Proceedings of the VLDB Conference, pp. 327–336. Morgan Kaufmann, San Francisco (1991)Google Scholar
  11. 11.
    Jacob, B., de Berg, J., Husiman, M., van Berkum, M.: Reasoning about Java classes. In: Proceedings of OOPSLA 1998, pp. 329–340. ACM Press, New York (1998)CrossRefGoogle Scholar
  12. 12.
    Java Core Reflection, JDK 1.1, Sun Microsystems (1997)Google Scholar
  13. 13.
    JavaTM Data Objects, JSR 000012, Forte Tools, Sun Microsystems Inc. (2000) Google Scholar
  14. 14.
    Jordan, M., Atkinson, M.: Orthogonal persistence for Java - A mid-term report. In: Morrison, R., Jordan, M., Atkinson, M. (eds.) Advances in Persistent Object Systems, pp. 335–352. Morgan Kaufmann Publishers, San Francisco (1999)Google Scholar
  15. 15.
    Lindholm, T., Yellin, F.: The JavaTM Virtual Machine Language Specification. Addison-Wesley, Reading (1996)Google Scholar
  16. 16.
    Liskov, B., Wing, J.M.: A behavioral notion of subtyping. ACM Transactions on Programming Languages and Systems 16, 1811–1841 (1994)CrossRefGoogle Scholar
  17. 17.
    Owre, S., Shakar, N., Rushby, J.M., Stringer-Clavert, D.W.J.: PVS Language Reference, SRI International, Computer Science Laboratory, Menlo Park, CaliforniaGoogle Scholar
  18. 18.
    Solorzano, J., Alagić, S.: Parametric polymorphism for JavaTM: A reflective solution. In: Proceedings of OOPSLA 1998, pp. 216–225. ACM Press, New York (1998)CrossRefGoogle Scholar
  19. 19.
    Sheard, T., Stemple, D.: Automatic verification of database transaction safety. ACM Transactions on Database Systems 14, 322–368 (1989)CrossRefGoogle Scholar
  20. 20.
    Spelt, D., Balsters, H.: Automatic verification of transactions on an object oriented database. In: Cluet, S., Hull, R. (eds.) DBPL 1997. LNCS, vol. 1369, pp. 396–412. Springer, Heidelberg (1998)Google Scholar
  21. 21.
    Spelt, D., Even, S.: A theorem prover-based analysis tool for object-oriented databases. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 375–389. Springer, Heidelberg (1999)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Suad Alagić
    • 1
  • Jeremy Logan
    • 1
  1. 1.Department of Computer ScienceUniversity of Southern MainePortlandUSA

Personalised recommendations