模型转换静态验证方法研究

Model transformaiton is an important approach to software development automation. In a model-driven development process, the correctness of model transformations decides whether or not the development will successed and effects the quality of the software system produced by the development. How to verify the correctness of a model transformation becomes a critical issue when model-driven approaches are applied. Current verification methods are usually not general purpose and lacks of soundness. Combined with the advance of the related researches, this project, which focuses on the verification of model transformation, intends to proposes a general static verification method of model transformations. First, by analyzing the features of current approaches, we will propose a general purpose theoretical model on static verfication of model transformations. The model specifies what information and operations are required during verification, which will be the foundation of the subsequent research. Second, we will investigate the commonality and variablity of model transformations and propose a unified abstract structure to increase the universality of our approach. And, to ensure the soundness of the verification process, we will also study how to describe the executable semantics of transformation langauges, the basis of static verification, precisely.At last, the project will design a systematic algorithm that is able to deduce the verification codes (i.e. the input of a verification tool) from the model transformation and the correctness property to be verifed in accordance with the executable semantics of the corresponding transformation langauge.

模型转换是实现软件开发自动化的重要途径。在一个模型驱动的开发过程中，模型转换的正确性将决定整个开发过程的成败，并影响最终生产出的软件制品的质量。如何验证模型转换的正确性成为了施展模型驱动开发方法时必须解决的一个关键问题。现有的验证方法缺乏通用性与合理性。结合相关技术的最新发展，本项目围绕模型转换的验证方法展开研究，提出一通用的静态验证方法。首先，通过广泛调研分析现有方法的特点，提出一种通用的理论验证模型，讨论验证模型转换过程中需要哪些信息和操作，为后续研究提供理论基础。其次，研究模型转换的共性和变化性，提出一种统一的抽象结构作为提高通用性的技术支撑。为了保证验证过程的合理性，研究如何精确刻画模型转换的可执行语义，提出一种基于OCL的可执行语义规约技术。最后，研究一种通用的系统化的翻译算法，可以根据可执行语义规约，将待检验的模型转换变换成一组OCL不变式。以便利用OCL约束求解器进行检。

模型转换是实现软件开发自动化的重要途径。在一个模型驱动的开发过程中，模型转换的正确性将决定整个开发过程的成败，并影响最终生产出的软件制品的质量。如何验证模型转换的正确性成为了施展模型驱动开发方法时必须解决的一个关键问题。现有的验证方法缺乏通用性与合理性。结合相关技术的最新发展，本项目围绕模型转换的验证方法展开研究，提出一通用的静态验证方法。项目首先通过理论分析建立了一个通用的模型转换静态验证框架，同时通过经验研究的方式调研了现有模型转换程序的设计质量以及亟需验证的性质。其次，项目通过对现有模型转换语言进行调研，提出了一种通用的模型转换语法表示和抽象解释引擎。最后，项目实现了一个模型转换验证原型工具，并发现其中存在的性能瓶颈问题，围绕该问题，深入地研究了模型自动生成问题。