JUCS - Journal of Universal Computer Science 15(11): 2196-2224, doi: 10.3217/jucs-015-11-2196
Checking Semantics Equivalence of MDA Transformations in Concurrent Systems
expand article infoPaulo Barbosa‡, Franklin Ramalho‡, Jorge Figueiredo‡, Aniko Costa§, Luis Gomes§
‡ Federal University of Campina Grande, Campina Grande, Brazil§ Universidade Nova de Lisboa, Lisboa, Portugal

Corresponding author: Paulo Barbosa ( paulo@dsc.ufcg.edu.br )

© Paulo Barbosa, Franklin Ramalho, Jorge Figueiredo, Aniko Costa, Luis Gomes.
This article is freely available under the J.UCS Open Content License.
Citation: Barbosa P, Ramalho F, Figueiredo J, Costa A, Gomes L (2009) Checking Semantics Equivalence of MDA Transformations in Concurrent Systems. JUCS - Journal of Universal Computer Science 15(11): 2196-2224. https://doi.org/10.3217/jucs-015-11-2196
Open Access
Abstract
In a previous work we have proposed an extension to the four-layer MDAarchitecture promoting formal verification for semantics preserving model transformations. We analyzed semantics equivalence in transformations involving Platform Specific Models (PSM s). In this paper, considering concurrent systems domain, we show how this extended MDA architecture copes with the correctness verification of horizontal model transformations involving Platform Independent Models (PIM s). Our approach is supported by four formal techniques: behavioral equivalence relation, category the-ory, bisimulation and model-checking. This set of techniques allows the analysis of semantics equivalence between system model before and after transformation enablingthe decomposition of the system model into a set of concurrent sub-models, considered as components. The validation of our approach occurs in a net splitting operation,where PIM s are defined as Petri nets models according to the PNML metamodel with transformations representing formal operations in this domain.
Keywords
MDA, transformations, formal semantics, concurrent systems, petri nets