Formal transformation of platform independent models into platform specific models

摘要: This paper introduces a method for formal transformation of platform independent models (PIM) to specific (PSM) in model driven architecture (MDA) context. The are constructed using state-machines the Unified Modeling Language (UML). As framework reasoning about we use Event B. In this illustrate our by introducing fault tolerance PSM. Fault is not considered PIM order make reusable different platforms. On other hand, PSM often has consider faults. However, mechanisms cannot usually be introduced as refinement We present preserve properties construction Design patterns used guiding development. Our can beneficial developing reliable applications many areas, since both UML and B practical applications.