A survey of approaches for verifying model transformations

被引:57
作者
Ab Rahim, Lukman [1 ]
Whittle, Jon [2 ]
机构
[1] Univ Teknol PETRONAS, Dept Comp & Informat Sci, Tronoh 31750, Perak, Malaysia
[2] Univ Lancaster, Sch Comp & Commun, InfoLab21, Lancaster LA1 4WA, England
关键词
Model transformations; Verification; Survey; SPECIFICATION; VERIFICATION; SEMANTICS; CONSTRUCTION; VALIDATION; PROOF;
D O I
10.1007/s10270-013-0358-0
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
As with other software development artifacts, model transformations are not bug-free and so must be systematically verified. Their nature, however, means that transformations require specialist verification techniques. This paper brings together current research on model transformation verification by classifying existing approaches along two dimensions. Firstly, we present a coarse-grained classification based on the technical details of the approach (e.g., testing, theorem proving, model checking). Secondly, we present a finer-grained classification which categorizes approaches according to criteria such as level of formality, transformation language, properties verified. The purpose of the survey is to bring together research in model transformation verification to act as a resource for the community. Furthermore, based on the survey, we identify a number of trends in current and past research on model transformation verification.
引用
收藏
页码:1003 / 1028
页数:26
相关论文
共 108 条
[11]  
Baudry B., 2006, ECMDA WORKSH INT MOD
[12]   MODELS@ RUN.TIME [J].
Blair, Gordon ;
Bencomo, Nelly ;
France, Robert B. .
COMPUTER, 2009, 42 (10) :22-27
[13]  
Blech J., 2005, FUJABA DAYS 2005, P49
[14]   VERIFYING AND VALIDATING SOFTWARE REQUIREMENTS AND DESIGN SPECIFICATIONS [J].
BOEHM, BW .
IEEE SOFTWARE, 1984, 1 (01) :75-88
[15]  
Boronat A, 2009, LECT NOTES COMPUT SC, V5503, P18
[16]   Specification and proof in membership equational logic [J].
Bouhoula, A ;
Jouannaud, JP ;
Meseguer, J .
THEORETICAL COMPUTER SCIENCE, 2000, 236 (1-2) :35-132
[17]  
Brooks F. P, 1995, MYTHICAL MAN MONTH A
[18]  
Brottier E, 2006, ISSRE 2006:17TH INTERNATIONAL SYMPOSIUM ON SOFTWARE RELIABILITY ENGINEERING, PROCEEDINGS, P85
[19]  
BUTH B, 1992, LECT NOTES COMPUT SC, V641, P141
[20]   Verification and validation of declarative model-to-model transformations through invariants [J].
Cabot, Jordi ;
Clariso, Robert ;
Guerra, Esther ;
de Lara, Juan .
JOURNAL OF SYSTEMS AND SOFTWARE, 2010, 83 (02) :283-302