With the growth of systems complexity the need for verifying the behavior of systems is increasing. UML per se provides no means to check model consistency. However, UML models can be checked if they are converted into their equivalent formal representation. In this paper, we propose an approach based on Model-to-Text transformation to perform a semi-automatic mapping for verification of concurrent UML models using MERL language and MetaEdit+ tool. State machine is transformed into SMV model description and activity diagram is transformed into LTL formulas. Then, we use NuSMV model checker to verify the obtained formal specification. To evaluate the work, a case study of the ordering system is presented to illustrate our approach. A mapping method to check the consistency of state machines with related activity diagrams at early stages of system development is the main result of our work.
Model to model transformation is a process of generating a target model from the source input model. However, after applying the transformation, both source and target models may evolve independently. In these cases, bidirectional transformation (Bx) is required to propagate changes across models to resolve the inter-model inconsistency. In this paper, we propose an interactive Bx approach via inter-model validation which enables developers synchronizing models with reconciliation. The proposed Bx system is implemented using the Epsilon Validation Language (EVL). A trace meta-model is designed to provide change propagation leads to bidirectional correspondence between models. The approach is formalized based on the synchronization concepts achieving 13 different states for each bidirectional relation. Our approach is compared to some other well-known Bx approaches considering six significant synchronization features. The results illustrate the appropriateness of the proposed approach.
In this paper, we identify model transformation specification and design patterns which support the property of transformation bidirectionality: the ability of a single specification to be applied either as a source-to-target transformation or as a target-to-source transformation.
The most widely-used model transformation languages, such as ATL and ETL, combine declarative and imperative aspects to define how one model is derived from another, or is updated in-place. General verification techniques for such languages must therefore be able to support reasoning about both declarative and imperative aspects. We define an analysis process which can, in principle, treat several different hybrid transformation languages, by making use of a common intermediate representation to express the semantics of transformations in any of these languages. Some analyses can be performed directly on the intermediate representation, and further semantic models in specific verification formalisms can be derived from it.
In this paper we identify model transformation specification and design patterns which support the property of transformation bidirectionality: the ability of a single specification to be applied either as a source-to-target transformation or as a target-to-source transformation.