特定领域建模(Domian-Specific Modeling, DSM)作为一种面向特定领域的模型驱动软件开发(Model-Driven Software Development, MDSD)方法,以特定领域分析和建模为核心并将领域模型看作软件开发的主要产品,因此在这种面向特定领域的模型驱动开发中,领域模型的质量决定了软件产品的质量。而作为领域模型质量最基本也最重要性质之一的领域模型的一致性及其验证问题,其研究和应用远不如UML成熟和深入,已成为特定领域建模领域的研究热点。由于采用非形式化方式定义的特定领域元建模语言和建模语言不具备对其结构特性和约束关系的严格描述能力且无法验证其自身的一致性,所以基于这种特定领域元建模语言和建模语言构建的特定领域模型的一致性验证只能采用硬编码方式或者经验规则方式,致使验证缺乏整体性、系统性和精确性。论文在前期研究的特定领域元建模语言XMML(XML-Based Meta-Modeling Language)的基础上,针对领域模型的一致性及其验证问题,对XMML进行了扩展和细化,给出了XMML元建模语言抽象语法和结构语义基于一阶逻辑的形式化表示,建立元模型在域范围内基于一阶逻辑的形式化框架以及采用元模型符号集定义领域一致性约束的定义机制,提出了基于元域的元模型一致性、基于域的元模型一致性、领域一致性约束的一致性和有效性以及基于域的模型一致性的概念及其基于一阶逻辑推演的验证方法,研究了元模型和模型到对应一组一阶逻辑公式的形式化自动映射机制并设计并实现了相应的自动映射原型程序,进而以软件体系结构和计算机网络拓扑结构的特定领域建模为例进行了实例研究,从而说明了该方法的可行性和实用性。本论文是对特定领域建模研究领域基于元建模语言形式化表示的元模型和模型可验证性方面的应用理论研究,为下一步在特定领域模型转换及领域代码生成方面的研究有重要的促进作用,具有一定的理论意义和实用价值。