Specification and verification of database dynamics

José Fiadeiro, Amílcar Sernadas

Research output: Contribution to journalArticlepeer-review

25 Citations (Scopus)


A framework is proposed for the structured specification and verification of database dynamics. In this framework, the conceptual model of a database is a many sorted first order linear tense theory whose proper axioms specify the update and the triggering behaviour of the database. The use of conceptual modelling approaches for structuring such a theory is analysed. Semantic primitives based on the notions of event and process are adopted for modelling the dynamic aspects. Events are used to model both atomic database operations and communication actions (input/output). Nonatomic operations to be performed on the database (transactions) are modelled by processes in terms of trigger/reaction patterns of behaviour. The correctness of the specification is verified by proving that the desired requirements on the evolution of the database are theorems of the conceptual model. Besides the traditional data integrity constraints, requirements of the form "Under condition W, it is guaranteed that the database operation Z will be successfully performed" are also considered. Such liveness requirements have been ignored in the database literature, although they are essential to a complete definition of the database dynamics.
Original languageEnglish
Pages (from-to)625-661
Number of pages37
JournalActa Informatica
Issue number6
Publication statusPublished - 1 Aug 1988


  • Conceptual model
  • Computational Mathematic
  • Structure Specification
  • Communication Action
  • Order Linear


Dive into the research topics of 'Specification and verification of database dynamics'. Together they form a unique fingerprint.

Cite this