Premium
Formal specification synthesis for relational database model
Author(s) -
Vatanawood Wiwat,
Rivepiboon Wanchai
Publication year - 2004
Publication title -
international journal of intelligent systems
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 1.291
H-Index - 87
eISSN - 1098-111X
pISSN - 0884-8173
DOI - 10.1002/int.10159
Subject(s) - computer science , relational model , mathematical proof , relational database , formal specification , theoretical computer science , formal methods , programming language , set (abstract data type) , database , mathematics , geometry
This article proposes an automatic scheme for synthesizing formal specification from the definitions of the relational data model—entity relationship diagram (ERD), and their data dictionaries. The formal specification of both structural and behavioral properties of the relational database model is generated in Z schemas. In our approach, the mandatory structural constraints—the uniqueness of primary key, foreign keys, and referential integrity constraints among the relations in the method—are preserved. We propose a set of transformation rules to exhaustively produce Z schemas of the states and primitive operations—cascade insertion, deletion, and updating. Moreover, in this article we focus on a composition technique of constructing the composite operations using the primitive composition tree. The revision of the formal specification can be conducted easily with the mathematical proofs of the properties of the data model using the Z prover tool. © 2004 Wiley Periodicals, Inc.