by Donatella Castelli and Elvira Locuratolo
ASSO, a Formal Database Design Methodology which combines features of the database area with formal methods, is now being defined at IEI-CNR. The methodology retains typical database models, thus permitting a flexible description of the conceptual schema and an efficient implementation, but at the same time guarantees the correctness of the design.
Methodologies currently used for database design do not guarantee correctness, i.e. they do not ensure that the implementation in the chosen database programming language satisfies the requirements specified in the conceptual schema. On the contrary, some recent formal methods proposed in the software engineering area support a correct development, but are not widely employed in the database area because they are too complex to be attractive when compared with the informal database methodologies.
ASSO, combines features of Database Design with the B formal method, in order to retain models and languages typical of the database area within the methodology while defining their formal semantics orthogonally. This makes the methodology accessible to non expert users of formal methods but at the same time properties can be proved by the designer if necessary.
ASSO consists of two stages: conceptual design and refinement.
In the conceptual design, both the structural and the behavioral requirements of the database are specified at a high level of abstraction, i.e. independently of implementational details. A Semantic Data tModel permits the conceptual schema to be specified in a flexible way. The conceptual schema has a two fold functionality: on the one hand, it is the starting point for refinement; on the other, the reference point for applications. This last functionality distinguishes the ASSO approach from those commonly used in the database area where the applications are written in terms of the logical schema description. An axiomatic definition of the semantic data model supporting this stage has been given exploiting the axiomatic definition of the model used by the B-Method. Desired properties of the conceptual schema, such as its consistency, can thus be proved.
The refinement stage transforms the conceptual schema into an object-oriented model that can be directly translated into the language accepted by the chosen Database Management System. This stage is defined by a data refinement} step and a sequence of transaction refinement steps. The data refinement step focuses on the transformation of the conceptual schema into an equivalent object schema whereas each transaction refinement reduces the nondeterminism and/or weakens the preconditions introduced when specifying the conceptual schema behaviour. The data refinement step is performed automatically by an algorithm which guarantees the correctness of the schema transformations, whereas formulas derived from corresponding B-Method formulas, must be applied to prove the correctness of the transaction refinement steps.
iei.pi.cnr.itiei.pi.cnr.it