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

项目名称： 模型转换静态验证方法研究

项目编号： No.61300009

项目类型： 青年科学基金项目

立项/批准年度： 2014

项目学科： 自动化技术、计算机技术

项目作者： 何啸

作者单位： 北京科技大学

项目金额： 22万元

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

中文关键词： 模型转换；静态验证；模型生成；；

英文摘要： 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 bas

英文关键词： Model Transformation；Static Verification；Model Generation；；