UML activity diagram to event-B: A model transformation approach based on the institution theory

Making jointly a semi formal language and a formal language can be seen as the transformation of a semi formal model into a formal model. Thus, this task can be considered as a model transformation from an abstract model into another concrete one. In this context, the paper at hand comes up with an approach to model transformation from a UML Activity Diagram (UML AD) into the Event-B model. The approach will be fully detailed in the paper by putting the stress on its different steps. The issue of semantic preserving during the transformation process will also be discussed. The latter is performed after defining two local semantics for the UML AD and Event-B specification. The mathematical foundation of our approach is the institution theory. Such a theory establishes a new notion of algebraic semantic for the source and target formalisms. Additionally, with the institution morphisms, we define a semantic correctness and coherence of the model transformation.