Within the MDA context, model transformations (MT) play an important role as they ensure consistency and significant time savings. Several MT frameworks have been deployed and successfully used in practice. Like for any software, the development of MT programs is error prone. However there is limited support for verification and validation in current MDA technologies. This paper presents an approach to prove model transformations. Model transformations are firstly formalized in B. Then the B provers will be used to analyze and prove the correctness of transformation rules w.r.t. met models and transformation invariants. We also analyze and prove the consistency of transformation rules w.r.t. each other.

In a development of real-time embedded systems, one needs to consider at very early stages the platform on which the systems are deployed. An explicit specification of system resources enables in fact the specification of non-functional properties. In this paper, as an attempt to define a formal component model for real-time embedded systems, we propose to use resources as the first-class citizen at the contract level of components. We show that this explicit specification of resources enables not only the flexibility of the component contract but also the specification of several non-functional properties of systems. We show a way that the worst case execution time (WCET) and the concurrency of component methods are expressed and validated in terms of resources that are available to the component in question.

In the continuity of our research on integration of UML and B, we address the transformation from OCL (Object Constraint Language), which is an integral part of UML, into B. Our derivation schemes allow to systematically even automatically derive into B not only the complementary class invariants, the statechart guard conditions, but also the OCL specification for UML operations.

Summary form only given. The research to merge the relatively simple and graphical nature of UML with the firm semantics bases of B has been mentioned several time in the literature. The goal is to propose automatic derivation schemes from UML to B specifications. Then, the construction of UML specifications is rigorously controlled by analyzing derived a specifications thanks to powerful B support tools. Dealing with the modeling UML behavioral diagrams in B, which has not been treated so far, is the main objective of the current work. We emphasize on the translation from use case, interaction and statechart diagrams into B specifications. We formalize each class operation, use case, event as a B operation which is encapsulated in a B abstract machine where are modeled the class data involved by the class operation, use case or event in question. In order to get the derived B specification more structured, we consider the class operation calling-called dependency, the use case structuring and the relation between events and its triggered transition. To complete the derivation schemes, we have proposed three derivation procedures based on class operations, use case and events I In addition, we have envisaged the following verifications on UML specifications: (i) the consistency of the class invariant; (ii) the conformity of object and state-chart diagrams regarding the class diagrams; (iii) the conformity of class operations, use cases regarding the class invariant; (iv) the class operation calling-called dependency and (v) the use case structuring.

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.