Specification and verification of database dynamics
type: Item
instance of: scholarly article
title: Specification and verification of database dynamics
zbMATH Open document ID: 0627.68078
DOI: 10.1007/BF00291052
author: Amílcar Sernadas
author: José Fiadeiro
published in: Acta Informatica
publication date: 1988-01-01T00:00:00Z
review text: 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). Non-atomic 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 rquirements have been ignored in the database literature, although they are essential to a complete definition of the database dynamics.
Mathematics Subject Classification ID: 68P20
Mathematics Subject Classification ID: 68Q65
zbMATH DE Number: 4020515
zbMATH Keywords: structured specification and verification of database dynamics
zbMATH Keywords: many sorted first order linear tense theory
zbMATH Keywords: conceptual modelling
zbMATH Keywords: liveness
MaRDI profile type: Publication
cites work: Towards a general theory of action and time
cites work: A Theory of Communicating Sequential Processes
cites work: The INFOLOG linear tense propositional logic of events and transactions
cites work: Q3332238
cites work: An axiomatic basis for computer programming
cites work: Q3777424
cites work: Verifying concurrent processes using temporal logic
cites work: Q5604443
cites work: Q5574489
cites work: Synthesis of Communicating Processes from Temporal Logic Specifications
cites work: Proving Liveness Properties of Concurrent Programs
cites work: Q4139641
cites work: Q4187287
cites work: Q3746875
cites work: Q5556395
cites work: Q5636857
cites work: Monitoring dynamic integrity constraints based on temporal logic
cites work: Towards multi-level and modular conceptual schema specifications
cites work: Temporal aspects of logical procedure definition
cites work: Q3745334
description: scientific article; zbMATH DE number 4020515