Abstract
We present a theorem-prover based analysis tool for object-oriented database systems with integrity constraints. Object-oriented database specifications are mapped to higher-order logic (HOL). This allows us to reason about the semantics of database operations using a mechanical theorem prover such as Isabelle or PVS. The tool can be used to verify various semantics requirements of the schema (such as transaction safety, compensation, and commutativity) to support the advanced transaction models used in workflow and cooperative work. We give an example of method safety analysis for the generic structure editing operations of a cooperative authoring system.
Research supported by SION, Stichting Informatica Onderzoek Nederland.
Chapter PDF
References
F. Bancilhon, C. Delobel, and P. Kanellakis, editors. Building an Object-oriented Database System: The Story of O2. Morgan Kaufmann, 1992.
M. Benedikt, T. Griffin, and L. Libkin. Verifiable properties of database transactions. In Proceedings of Principles of Database Systems (PODS), pages 117–127, 1996.
V. Benzaken and X. Schaefer. Static management of integrity in object-oriented databases: Design and implementation. In Extending Database Technology (EDBT), March 1998.
A. J. Bernstein, D. S. Gerstl, W.-H. Leung, and P. M. Lewis. Design and performance of an assertional concurrency control system. In Proceedings of ICDE, pages 436–445, Orlando, Florida, February 1998.
R. G. G. Cattell and Douglas K. Barry, editors. The Object Database Standard: ODMG 2.0. Morgan Kaufmann Publishers, San Francisco, California, 1997.
M. Doherty, R. Hull, M. Derr, and J. Durand. On detecting conflict between proposed updates. In International Workshop on Database Programming Languages (DBPL), Gubbio, Italy, September 1995.
Isabelle. http://www.cl.cam.ac.uk/Research/HVG/isabelle.html.
B. Jacobs, J. van den Berg, M. Huisman, M. van Berkum, U. Hensel, and H. Tews. Reasoning about Java Classes (Preliminary Report). In Proceedings of OOPSLA, 1998. To appear.
Cris Pedregal Martin and Krithi Ramamritham. Delegation: Efficiently rewriting history. In Proceedings of ICDE, pages 266–275, Birmingham, U.K., April 1997.
Lawrence C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of LNCS. Springer-Verlag, 1994.
Xiaolei Qian. The deductive synthesis of database transactions. ACM Transactions on Database Systems, 18(4):626–677, December 1993.
Marek Rusinkiewicz, Wolfgang Klas, Thomas Tesch, Jürgen Wäsch, and Peter Muth. Towards a cooperative transaction model-The Cooperative Activity Model. In Proceedings of the 21st VLDB Conference, Zurich, Switzerland, September 1995.
Thomas Santen. A theory of structured model-based specifications in Isabelle/HOL. In Proc. of the 1997 International Conference on Theorem Proving in Higher Order Logics (TPHOLs97), Lecture Notes in Computer Science. Springer-Verlag, 1997.
Tim Sheard and David Stemple. Automatic verification of database transaction safety. ACM Transactions on Database Systems, 14(3):322–368, September 1989.
David Spelt and Herman Balsters. Automatic verification of transactions on object-oriented databases. In Proceedings of the Workshop on Database Programming Languages (DBPL), Estes Park, Colorado, 1997.
N. Streitz, J. Haake, J. Hannemann, A. Lemke, W. Schuler, H. Schuett, and M. Thuering. SEPIA: A cooperative hypermedia authoring environment. In ACM Conference on Hypertext (ECHT), pages 11–22, Milano, Italy, 1992.
Jürgen Wäsch and Wolfgang Klas. History merging as a mechanism for concurrency control in cooperative environments. In IEEE Workshop on Research Issues in Data Engineering: Interoperability of Nontraditional Database Systems, pages 76–85, 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Spelt, D., Even, S. (1999). A Theorem Prover-Based Analysis Tool for Object-Oriented Databases. In: Cleaveland, W.R. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 1999. Lecture Notes in Computer Science, vol 1579. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49059-0_26
Download citation
DOI: https://doi.org/10.1007/3-540-49059-0_26
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65703-3
Online ISBN: 978-3-540-49059-3
eBook Packages: Springer Book Archive