特定领域元建模语言的形式化及其元模型和模型的一致性验证研究

In Domian-Specific Modeling(DSM) as a Model-Driven Development methodology for the specific domain, quality of model determines quality of software product, model's consistency as one of the basic and most important properties of model quality and its verification have become research hotspot.However,Domian-Specific Meta-Modeling Language defined by informal method can not strictly represent its structure characteristics and constraint relationships, so consistency of metamodels and models cannot be holistically and systematically and accurately verified. In response, based on expansion and refinement of Domian-Specific Meta-Modeling Language-XMML, the project presents a formal definitions based on first-order logic of structural semantics of XMML and establishes a formal framework for metamodel based on first-order logic and a definition mechanism of domain consistency constraints, based on this, it proposes concepts and verification methods based on first-order logical inference of consistency of metamodels and models and consistency and validity of domain consistency constraints, and then studies automatic mapping mechanism of formalisation of metamodels and models and designs and implements the corresponding automatic mapping engine,finally, it performs tests on the automatic mapping and verification to show the feasibility of our formal method. As the study of the applied theory for verification of metamodels and models based on formalisation of meta-modeling language, this project can greatly promote further researching of domain model transformation and domain codes making.

在特定领域建模这种面向特定领域的模型驱动开发方法中，模型的质量决定了软件产品的质量。而作为模型质量最重要性质之一的模型一致性及其验证问题，成为研究热点。然而非形式化定义的特定领域元建模语言不具备对其结构特性和约束关系的严格描述能力，致使元模型和模型的一致性验证缺乏整体性、系统性和精确性。本项目在对特定领域元建模语言XMML进行扩展和细化的基础上，给出XMML结构语义基于一阶逻辑的形式化表示，建立元模型基于一阶逻辑的形式化框架和领域一致性约束的自定义机制，基于此给出元模型和模型一致性以及领域一致性约束一致性和有效性的概念及其基于一阶逻辑推理的验证方法，研究元模型和模型形式化自动映射机制并设计和实现相应的自动映射引擎，最后实施自动映射和验证实验来说明我们形式化方法的可行性。本项目是基于元建模语言形式化表示的元模型和模型可验证性方面的应用理论研究，为模型转换及代码生成方面的研究有重要的促进作用。

在特定领域元建模和特定领域建模这种面向特定领域的模型驱动开发方法中，模型的质量决定了软件产品的质量。而作为模型质量最重要性质之一的模型逻辑一致性及其验证问题，成为研究热点。然而非形式化定义的特定领域元建模语言不具备对其结构特性和约束关系的严格描述能力，致使元模型和模型的逻辑一致性验证缺乏整体性、系统性和精确性。本项目首先对我们团队构建的特定领域元建模语言XMML进行了扩展和细化，在建立域和元域概念的基础上，完成了XMML结构语义基于一阶逻辑的形式化表示，进而建立了元模型基于一阶逻辑的形式化框架和领域约束的自定义机制，提出了元模型和模型逻辑一致性概念及其基于一阶逻辑推理的验证方法以及领域约束逻辑一致性和有效性的概念及其基于一阶逻辑推理的验证方法，基于此，构建了元模型和模型形式化自动映射机制并设计和实现了相应的元模型和模型形式化自动映射引擎，最后，我们针对软件体系结构和网络拓扑结构等若干完整元模型及其模型实例，进行了元模型和模型形式化自动映射实验以及元模型和模型逻辑一致性验证实验，实验表明，特定领域元建模语言XMML的形式化表示机制是有效的，基于XMML形式化表示的元模型和模型逻辑一致性验证方法是可行的。本项目是基于元建模语言形式化表示的元模型和模型可验证性方面的应用理论研究，而模型的可验证性是保证模型质量的一种重要机制，从而为下一步进行模型高质量转换以及高质量代码自动生成奠定了坚实的基础。