Mapping Object Diagrams into B Specifications

In this paper we study the combination of object-oriented and formal methods and more specifically the mapping of object models, that are used in business information system development methods, into the formal specification language of the B method. We retain as the starting point of our study a common core of object concepts accepted by most of the groups: object, entity, association, is-a link. The first aim is to formalize these concepts. The main idea is to organize the specification around sets of object identities. Thus associations are modelled using relations between these sets and is-a links are modelled by inclusion constraints between these sets. The second aim is to modularise the final formal specification. Our purpose is to keep as much as possible the initial object diagram structure in the formal specification. Thus each entity is mapped into one abstract machine, an association is put in a specific machine according to its own properties, inheritance is simulated by using the existing links between abstract machines.