一个模型转换的验证框架

模型驱动体系结构（Model Driven Architecture，MDA）是OMG为充分利用基于UML的建模技术并分离软件系统的抽象描述和具体事项而提出的。模型转换对MDA的成功至关重要，但对于同传统软件开发过程中的测试部分同等重要的模型转换中的验证和有效性确认（V＆V），目前的研究比较少。为此，尝试提供一个基于MDA上下文的模型转换性能的验证框架。该框架用于验证原模型包涵的性质，检查源模型与／或目标模型的各个元素是否通过模型转换规则实现了语义等价。同时，采用EMFAPI开发了一个用来分析Tefkat语言描述的模型转换规则的verifier原型系统，并通过实例验证了其有效性。

A Framework for Verifying Model Transformations

Model Driven Architecture （MDA） is an initiative issued by the OMG to leverage UML-based modelling techniques to insulate abstract software system specifications from implementation dependencies. Model transformation is a key concept and vital for the success of MDA. But little has been done on Verification and Validation （V＆V） of model transformations, which is as critical as the testing stage in the traditional software development process. This paper attempts to tackle this problem by providing a verification framework which can verify model transformations against properties. The framework is applied to the property of metamodel coverage, checking how elements of source and/or target metamodel are covered by model transformation rules. A prototype verifier has been developed using the EMF APIs to analyze transformation rules specified in the Tefkat language. Applying this verifier to the example model transformation, we get the effective output of the framework.