Abstract: Verification of model processing programs, where only the definitions of the program and the languages of the models to be transformed are analyzed, has become a fundamental issue in model-based software engineering. This analysis may become very complex, but it is performed only once and the results are independent from concrete input models. The formal background of verification methods for graph rewriting-based model transformations has become a subject of research recently. In previous work, we have provided fundamental formal and algorithmic background of a (semi-)automated verification approach for graph transformations. This work concludes these components and put them together to introduce the implementation of a verification system fully integrated into a model transformation framework, VMTS. The strong points of our approach is its usability, its implementation in an existing tool, and its extendibility, which are demonstrated on a case study in the application domain of mobile centric social networks. Our results show that the verification of graph rewriting-based model transformations can be largely automated.
Abstract: Model-based development is one of the most promising solutions for several problems of industrial software engineering. Graph transformation is a proven method for processing domain-specific models. However, in order to be used by domain experts without graph transformation experts, it must be fast even if not tweaked for speed manually based on knowledge available only to the implementers of the transformation system. In this paper, we compare the performance of such manual optimizations with a solution using automated optimization based on sharing of matches between overlapping left-hand-sides of sequentially independent rules. This yields a 11% improvement in our scenario, although our prototypical implementation only exploits overlapping between, at most, two rules, and the analyzed benchmark does not contain many cases where the optimization is applicable.
Abstract: The Multi-Paradigm Modeling (MPM) approach of model-based development emphasizes the specification of a system by multiple models. We use transformations to automatically transform, integrate and synchronize models. Verification and validation of model transformations are fundamental issues: we need to express what a valid model is and how a valid model transformation may transform the models; otherwise, we have to analyze each transformed model individually, which makes it difficult to automate the process of using models. We have formally analyzed various model transformations in several case studies and industrial projects. From this experience, we have distilled the frequently recurring techniques and solutions, referred to as Model Transformation Analysis (MTA) methods. These instances, similarly to design patterns in object-oriented programming, define special constructions as solutions for recurring problems that arise when one implements a model transformation. Moreover, MTA methods contain special techniques and language features that should be taken into account when one designs a model transformation framework or a model transformation language. We hope that MTA methods may be the basis of automated formal analysis techniques of model transformations. This paper contributes the concept and instances of MTA methods and provides a case study based on an industrial project of mobile application development. With this real-world example, we want to demonstrate the role and use of MTA methods. The case study is implemented in Visual Modeling and Transformation System (VMTS), which is a tool that realizes the MPM concept to provide a model and model transformation-based environment for software development.
Abstract: Verification of the transformations is a fundamental issue for applying
them in real world solutions. We have previously proposed a formalization to declaratively
describe model transformations and proposed an approach for the verification.
Our approach consists of a reasoning system that works on the formal transformation
description and deduction rules for the system. The reasoning system can
automatically generate the proof of some properties. In this paper, we present a case
study, to demonstrate our approach of automated verification of model transformations
in a multi-paradigm environment.
Abstract: Verification of the transformations is a fundamental issue for applying
them in real world solutions. We have previously proposed a formalization to declaratively
describe model transformations and proposed an approach for the verification.
Our approach consists of a reasoning system that works on the formal transformation
description and deduction rules for the system. The reasoning system can
automatically generate the proof of some properties. In this paper, we present a case
study, to demonstrate our approach of automated verification of model transformations
in a multi-paradigm environment.
Abstract: Verification of models and model processing programs are inevitable in real-world model-based software development. Model transformation developers are interested in offline verification methods, when only the definition of the model transformation and the metamodels of the source and target languages are used to analyze the properties and no concrete input models are taken into account. Therefore, the results of the analysis hold for each output model not just particular ones, and we have to perform the analysis only once. Most often, formal verification of model transformations is performed manually or the methods can be applied only for a certain transformation or for the analysis of only a certain property. Previous work has presented a formalism to describe the characteristics of model transformations in separate formal expressions called assertions. This description is based on the first-order logic, therefore, if deduction rules are provided, a reasoning system can use an assertion set to automatically derive additional assertions describing additional properties of model transformations. In this paper, we propose deduction rules and present the verification of a model transformation of processing business process models.
Abstract: Verification of models and model processing programs are inevitable in real world model-based software development. Model transformation developers are often interested in offline verification methods, when only the definition of the model transformation and the specification of the source and target languages are used to analyze the properties and no concrete input models are taken into account. Therefore, the results of the analysis hold for each output model not just particular ones, and we have to perform the analysis only once. Most often, formal verification of model transformations is performed manually or the methods can be applied only for a certain transformation or for the analysis of only a certain property. Previous work has presented formal and algorithmic background for a possible verification framework. Based on this background, this paper introduces a realization of an automated verification framework for graph rewriting-based model transformations. We illustrate the operation of the framework and demonstrate its applicability on a case study. Our goal is to further improve our approach in order to be able to be applied in more complex industrial solutions as well.
Abstract: Verification of models and model processing programs are inevitable in real world model-based software development. Model transformation developers are often interested in offline verification methods, when only the definition of the model transformation and the specification of the source and target languages are used to analyze the properties and no concrete input models are taken into account. Therefore, the results of the analysis hold for each output model not just particular ones, and we have to perform the analysis only once. Most often, formal verification of model transformations is performed manually or the methods can be applied only for a certain transformation or for the analysis of only a certain property. Previous work has presented formal and algorithmic background for a possible verification framework. Based on this background, this paper introduces a realization of an automated verification framework for graph rewriting-based model transformations. We illustrate the operation of the framework and demonstrate its applicability on a case study. Our goal is to further improve our approach in order to be able to be applied in more complex industrial solutions as well.
Abstract: Verification of models and model processing programs are inevitable in real-world model-based software development. Model transformation developers are interested in offline verification methods, when only the definition of the model transformation and the metamodels of the source and target languages are used to analyze the properties and no concrete input models are taken into account. Therefore, the results of the analysis hold for each output model not just particular ones, and we have to perform the analysis only once. Most often, formal verification of model transformations is performed manually or the methods can be applied only for a certain transformation or for the analysis of only a certain property. Previous work has presented a formalism to describe the characteristics of model transformations in separate formal expressions called assertions. This description is based on the first-order logic, therefore, if deduction rules are provided, a reasoning system can use an assertion set to automatically derive additional assertions describing additional properties of model transformations. In this paper, we propose deduction rules and present the verification of a model transformation of processing business process models.
Abstract: This paper presents the design, architecture, and implementation experiences related to building a multipurpose modeling and model transformation frameworks. We examine the usual expectations related to model-driven development tools, then we present the architecture and design decisions of a new modeling framework capable of fulfilling all these expectations. The suggested architecture and the provided implementation offer an approach that (i) has an efficient data structure, (ii) can be easily customized and (iii) optimized for different purposes of modeling.
Abstract: Verification of models and model processing programs are fundamental issues
and are inevitable in model-based software development in order to apply them in realworld
solutions. Verification concerns the analysis of non-functional and functional
properties as well. Model transformation developers are interested in offline methods for
the verification process. Offline analysis means that only the definition of the model
transformation and the metmodels of the source and target languages are used to analyze
the properties and no concrete input models are taken into account. Therefore, the results
of the analysis hold for each output model not just particular ones, and we have to perform
the analysis only once. Most often, formal verification of model transformations is
performed manually, but automated or semi-automated approaches have gained focus
recently. We have previously presented a method to formally describe the main
characteristics of model transformations. Our concept consists of two steps: (i) The
automatic generation of a formal description from a concrete transformation, which is
manually extended by formal assertions by transformation experts. (ii) A reasoning system
is used to automatically derive the proof of certain properties from the previous formal
description. In this paper, we show how deduction rules of the reasoning system can be
defined.
Abstract: This paper presents the design, architecture, and implementation experiences related to building a multipurpose modeling and model transformation frameworks. We examine the usual expectations related to model-driven development tools, then we present the architecture and design decisions of a new modeling framework capable of fulfilling all these expectations. The suggested architecture and the provided implementation offer an approach that (i) has an efficient data structure, (ii) can be easily customized and (iii) optimized for different purposes of modeling.
Abstract: Verification of models and model processing programs are inevitable in model-based software development in order to apply them in real-world solutions. Verification of properties of model transformations means to prove that the application of a model transformation generates the expected output models from the input models. Model transformation developers are interested in offline methods for the verification process. Offline analysis means that only the definition of the model transformation and the metmodels of the source and target languages are used to analyze the properties and no concrete input models are taken into account. Therefore, the results of the analysis hold for each output model not just particular ones, and we have to perform the analysis only once. Most often, formal verification of model transformations is performed manually or the methods can be applied only for a certain transformation or for the analysis of only a certain property. In this paper, we propose a formalization to describe model transformation. A formal description can be automatically generated, and can be extended by the experts. An automated reasoning system may prove some properties of model transformations by deriving new assertions from the original description.
Abstract: Verification of models and model processing programs are fundamental issues
and are inevitable in model-based software development in order to apply them in realworld
solutions. Verification concerns the analysis of non-functional and functional
properties as well. Model transformation developers are interested in offline methods for
the verification process. Offline analysis means that only the definition of the model
transformation and the metmodels of the source and target languages are used to analyze
the properties and no concrete input models are taken into account. Therefore, the results
of the analysis hold for each output model not just particular ones, and we have to perform
the analysis only once. Most often, formal verification of model transformations is
performed manually, but automated or semi-automated approaches have gained focus
recently. We have previously presented a method to formally describe the main
characteristics of model transformations. Our concept consists of two steps: (i) The
automatic generation of a formal description from a concrete transformation, which is
manually extended by formal assertions by transformation experts. (ii) A reasoning system
is used to automatically derive the proof of certain properties from the previous formal
description. In this paper, we show how deduction rules of the reasoning system can be
defined.
Abstract: The proliferation of Mobile P2P systems made a next generation mobile BitTorrent client an appropriate target to compare two different development approaches: the traditional manual coding and domain-specific modeling languages (DSMLs) accompanied by generators. We present two DSMLs for mobile communication modeling, and one for user interface development. We compare the approaches by development time and maintenance, using our modeling and transformation tool Visual Modeling and Transformation System (VMTS).
Abstract: Verification of models and model processing programs are inevitable in model-based software development in order to apply them in real-world solutions. Verification of properties of model transformations means to prove that the application of a model transformation generates the expected output models from the input models. Model transformation developers are interested in offline methods for the verification process. Offline analysis means that only the definition of the model transformation and the metmodels of the source and target languages are used to analyze the properties and no concrete input models are taken into account. Therefore, the results of the analysis hold for each output model not just particular ones, and we have to perform the analysis only once. Most often, formal verification of model transformations is performed manually or the methods can be applied only for a certain transformation or for the analysis of only a certain property. In this paper, we propose a formalization to describe model transformation. A formal description can be automatically generated, and can be extended by the experts. An automated reasoning system may prove some properties of model transformations by deriving new assertions from the original description.
Abstract: The transformation from UML activity diagrams to CSP models is a helpful
model transformation, which can be used to analyze and verify some aspects of a UML
activity diagrams. A working solution has been developed with our tool, the Visual
Modeling and Transformation System, and in this work we formally prove that the
transformation terminates for every valid input activity diagram model, and therefore it can
be used in practice.
Abstract: The transformation from UML activity diagrams to CSP models is a helpful
model transformation, which can be used to analyze and verify some aspects of a UML
activity diagrams. A working solution has been developed with our tool, the Visual
Modeling and Transformation System, and in this work we formally prove that the
transformation terminates for every valid input activity diagram model, and therefore it can
be used in practice.
