|
 
|
[LM00] Using a Formal Refinement to Derive Relational Database Implementations from B Specifications
Rapport Scientifique : Date de dépot: 2000/01/01, (Tech. Rep.: CEDRIC-00-86)
motcle:
Résumé:
In this paper, an approach for refining B abstract
specifications describing data-intensive
applications into relational database
implementations is presented. Using the refinement
process of the B method, a set of generic refinement
rules are described that take into account both
data and operations. The last step consists of
mapping the final refined component into a
relational database implementation. The different
rules have been checked with the AtelierB prover.
The aim of the work is to automate the refinement
steps. This is possible thanks to the genericity
feature of the rules. The approach is illustrated
through a running example.
Commentaires:
, extended version of the ZB2000 paper.
BibTeX
| @techreport { | |||
| LM00, | |||
| title | = | "{Using a Formal Refinement to Derive Relational Database Implementations from B Specifications}", | |
| author | = | "R. Laleau and A. Mammar", | |
| number | = | "{CEDRIC-00-86}", | |
| institution | = | "{CEDRIC laboratory, CNAM-Paris, France}", | |
| date | = | {01-01-2000}, | |
| note | = | "{, extended version of the ZB2000 paper.}", | |
| } | |||
