Verification and validation of declarative model-to-model transformations through invariants

被引:69
作者
Cabot, Jordi [2 ]
Clariso, Robert [2 ]
Guerra, Esther [1 ]
de Lara, Juan [3 ]
机构
[1] Univ Carlos III Madrid, Dept Comp Sci, E-28903 Getafe, Spain
[2] Multimedia & Telecomunicacio Univ, Oberta De Catalunya, Spain
[3] Univ Autonoma Madrid, Polytech Sch, E-28049 Madrid, Spain
关键词
Model-to-model transformation; Model-Driven Development; OCL; Verification and validation; Triple Graph Grammars; QVT;
D O I
10.1016/j.jss.2009.08.012
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
In this paper we propose a method to derive OCL invariants from declarative model-to-model transformations in order to enable their verification and analysis. For this purpose we have defined a number of invariant-based verification properties which provide increasing degrees of confidence about transformation correctness, such as whether a rule (or the whole transformation) is satisfiable by some model, executable or total. We also provide some heuristics for generating meaningful scenarios that can be used to semi-automatically validate the transformations. As a proof of concept, the method is instantiated for two prominent model-to-model transformation languages: Triple Graph Grammars and QVT. (C) 2009 Elsevier Inc. All rights reserved.
引用
收藏
页码:283 / 302
页数:20
相关论文
共 49 条
[1]  
AKEHURST DH, 2003, J SOFTWARE SYSTEMS M, V2, P215
[2]  
Anastasakis K., 2007, ModeVVa'07, P47
[3]  
Anastasakis K, 2007, LECT NOTES COMPUT SC, V4735, P436
[4]  
[Anonymous], LNCS
[5]  
Baresi L, 2006, LECT NOTES COMPUT SC, V4178, P306
[6]   Reasoning on UML class diagrams [J].
Berardi, D ;
Calvanese, D ;
De Giacomo, G .
ARTIFICIAL INTELLIGENCE, 2005, 168 (1-2) :70-118
[7]  
Bézivin J, 2006, LECT NOTES COMPUT SC, V4199, P440
[8]  
Binder RV., 1999, Testing Object-Oriented Systems: Models, Patterns, and Tools
[9]  
Brottier E, 2006, ISSRE 2006:17TH INTERNATIONAL SYMPOSIUM ON SOFTWARE RELIABILITY ENGINEERING, PROCEEDINGS, P85
[10]  
Brucker A. D, 2006, Tech. Rep., 525