Database design based on B

This chapter is devoted to the integration of the ASSO features in B. ASSO is a database design methodology defined for achieving conceptual schema consistency, logical schema correctness, flexibility in reflecting the real life changes on the schema and efficiency in accessing and storing information. Starting from a B specification of the data structure and of the transactions allowed on a database, two model transformations are designed. The obtained model integrates statics and dynamics exploiting the concepts of Class-Machines and Specialized Class-Machines, two concepts enriching corresponding concepts supported by the database conceptual languages. Formal details which must be specified if the conceptual model of ASSO is directly constructed in B are avoided; large consistency obligations are reduced to small obligations. Class Machines supported by semantic data models can be correctly linked with Class-Machines supported by object Models.