KIT | KIT-Bibliothek | Impressum
Open Access Logo
§
Volltext
URN: urn:nbn:de:swb:90-AAA3943

Translating E/R-diagrams into consistent database specifications

Fuchss, Thomas

Abstract:

Semi formal methods, for example those which are used
in the database community, are useful for communication between
developers and clients. But they are not useful for formal
verification.To overcome this problem it is possible to translate

E/R-diagrams into first order algebraic specifications. The aim of

our task was to prove the consistency of such translate
specifications. To realize the proof we use the KIV (Karlsruhe
Interactive Verifier) approach for the development of correct

large software systems, i.e. we prove the consistency indirect by

proving the correctness of an implementation. For this purpose we
automatically translate E/R-diagrams not only in an algebraic
specification, but in a modular system containing structured
specifications and implementations. For a concrete E/R-diagram we
can prove the correctness with the KIV system. Because the
translation is uniform a generalized handmade proof for arbitrary
but fixed E/R-diagrams is possible, and presented in this paper.

This paper also includes an exemplary translation of an
E/R-diagram with 5 entities and 6 relations. The generated modular
system contains 33 ... mehr


Zugehörige Institution(en) am KIT Institut für Logik, Komplexität und Deduktionssysteme (ILKD)
Publikationstyp Buch
Jahr 1994
Sprache Englisch
Identifikator KITopen ID: 394
Erscheinungsvermerk Karlsruhe 1994. (Interner Bericht. Fakultät für Informatik, Universität Karlsruhe. 1994,2.)
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft KITopen Landing Page