Title
A formalism for describing modeling transformations for verification
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.
Year
DOI
Venue
2009
10.1145/1656485.1656487
Proceedings of the 6th International Workshop on Model-Driven Engineering, Verification and Validation
Keywords
DocType
Citations 
expected output model,modeling transformation,concrete input model,model transformation,model processing program,model transformation developer,analysis hold,input model,offline analysis,output model,certain transformation,automated reasoning,benchmarking,software development,scalability,formal verification,statistical significance,uml class diagram
Conference
4
PageRank 
References 
Authors
0.56
6
3
Name
Order
Citations
PageRank
Márk Asztalos110810.94
László Lengyel217225.15
Tihamér Levendovszky318514.96