KIT | KIT-Bibliothek | Impressum | Datenschutz

Translating E/R-diagrams into consistent database specifications

Fuchss, Thomas


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 specifications with more than 300 specified
... mehr

Cover der Publikation
Zugehörige Institution(en) am KIT Fakultät für Informatik – Institut für Logik, Komplexität und Deduktionssysteme (ILKD)
Publikationstyp Buch
Publikationsjahr 1994
Sprache Englisch
Identifikator urn:nbn:de:swb:90-AAA3943
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