Stepwise specification of dynamic database behaviour

ABSTRACT

This paper presents a methodology for the stepwise specification of dynamic database behaviour. A conceptual schema is described in three levels: data, objects and transactions. To determine which sequences of database states are “admissible”, integrity constraints on objects are given in temporal logic. Transactions are specified by pre/postconditions to produce “executable” state sequences. In order to guarantee that executable state sequences already become admissible, integrity constraints are completely transformed into additional pre/postconditions. We introduce general rules for these transformations. Thus, schema specifications can be refined and simplified systematically.

REFERENCES

• FODS: Froc. ACM Symp. on Prlnclples of Database Systems
• SIGMOD: Froc. Int. ACM-SIGMOD Conf. on Management of Data
• TFAIS: Froc. IFIP Work. Conf.on Theoretlcal and Formal Aspects of Informatlon Systems (A.Sernadas et al. , eds. ) , North-Holland, Amsterdam 1985
• VLDB: Froc. Int. Conf. on Very Large Data Bases
• CCF82: José Mauro V. de Castilho , Marco A. Casanova , Antonio L. Furtado, A Temporal Framework for Database Specifications, Proceedings of the 8th International Conference on Very Large Data Bases, p.280-291, September 08-10, 1982
• CVF84: Marco A. Casanova , Paulo A. S. Veloso , Antonio L. Furtado, Formal data base specification: an eclectic perspective, Proceedings of the 3rd ACM SIGACT-SIGMOD symposium on Principles of database systems, April 02-04, 1984, Waterloo, Ontario, Canada [doi>10.1145/588011.588028]
• Ce83: Cer1,S. (ed.) : Methodology and Tool s f or Data Base Desl gn. North- Hol land, Amsterdam 1983
• ELG84: Hans-Dieter Ehrich , Udo W. Lipeck , Martin Gogolla, Specification, Semantics, and Enforcement of Dynamic Database Constraints, Proceedings of the 10th International Conference on Very Large Data Bases, p.301-308, August 27-31, 1984
• Fu84: A. L. Furtado, An informal approach to formal specifications, ACM SIGMOD Record, v.14 n.1, p.45-54, 1983 [doi>10.1145/984540.984544]
• GM79: Gardarln,G./Melkanof~,M.: Provlng Consistency of Database Transact# ons. VLDB 1979, 291-298
• ISO82: ISO/TC97/SC5/WG3 : Concepts and Termlnology ~or the Conceptual Schema and the I n# ormat i on Base. (J. J. van Grlethuysen, ed.) 1982
• Ku84: David Chenho Kung, A Temporal Framework for Database Specification and Verification, Proceedings of the 10th International Conference on Very Large Data Bases, p.91-99, August 27-31, 1984
• Ku85a: Kung, C.H. : A Tableaux Approach for Conslstency Checklng. TFAIS 1985, 191-210
• Ku85b: C. H. Kung, On verification of database temporal constraints, ACM SIGMOD Record, v.14 n.4, p.169-179, May 1985
• LEG85: LI peck ~ U.W. / Ehr I ch, H. -D. / Gogolla,M. : Specl fylng Admlsslb111ty of Dynam# c Database Behavl our Usl ng Temporal Loglc. TFAIS 1985, 145-157
• LSE86: LI peck ,U. W./Saake,G./Ehrl ch ,H. D. : Monl torl ng Dynaml c Database Integrl ty by Transltlon Graphs. 1986 (submltted for publlcatlon)
• MP81: Manna, Z./Pnuell ,A. : Verlflcatlon of Concurrent Programs: The Temporal Framework. In: The Correctness Problem In Computer Sclence (R.S. Boyer/ J.S. Moore, eds. ) , Academlc Press, 1981, 215-27_#
• Ni82: N1colas,J.-M.: Loglc for Improving Integrlty Checklng in Rel atlonal Data Bases. Acta Informatlca 18 (1982), 227-253
• SFNC84: Ulrich Schiel , Antonio L. Furtado , Erich J. Neuhold , Marco A. Casanova, Towards multi-level and modular conceptual schema specifications, Information Systems, v.9 n.1, p.43-57, 1984 [doi>10.1016/0306-4379(84)90015-2]
• TF82: Toby J. Teorey , James P. Fry, Design of Database Structures, Prentice Hall Professional Technical Reference, 1982
• VCF81: Vel oso, P. A. S. / Cast i I ho, J. M. V. de/ Furtado,A.L.: Systematlc Derlvatlon of Complementary Specflcatlons. VLDB 1981~ 409-421
• VF85: Veloso~P.A.S./ Furtado,A.L.: Towards Simpler and Yet Complete Formal Speclflcatlons. TFAIS 1985, 175-189

INDEX TERMS

Classification:
  H. Information Systems
  H.2 DATABASE MANAGEMENT
      H.2.0 General
          Subjects: Security, integrity, and protection**
      H.2.1 Logical Design
          Subjects: Schema and subschema

General Terms:
Design, Security