Modeling class operations in B: Application to UML behavioral diagrams

An appropriate approach for translating UML to B formal specifications allows one to use UML and B jointly in a unified, practical and rigorous software development. We formally analyze UML specifications via their corresponding B formal specifications. This point is significant because B support tools like AtelierB are available. We can also use UML specifications as a tool for building B specifications, so the development of B specifications become easier In this paper we address the problem of automatic derivation from UML behavioral diagrams into B specifications, which has been so far an open issue. A new approach for modeling class operations in B is presented Each class operation is mapped into a B operation. A class operation and its involved data are mapped into the same B abstract machine (BAM). The class operation calling-called dependency is used to arrange derived B operations into BAMs. For each calling-called pair of class operations, the B operation of the called operation participates in the implementation of the B operation of the calling operation.