图形化模型用图形来描述被研究系统的结构和行为,具有直观易懂的特点,在软件工程的研究和实践中得到广泛使用。随着模型驱动的软件开发方法的日益成熟和推广,一致性作为模型质量的一个基本性质日益受到人们的关注,成为近年来软件研究的热点。然而,由于图形化建模语言的非形式化的定义,当前对模型一致性检查的研究依然建立在经验规则的基础上。本文提出一种以建模语言的抽象语法和语义的形式化定义为基础、系统地解决模型一致性检查问题的途径,研究了其理论基础,提出了相应的实现技术,开发了软件原型系统,并以面向对象建模语言UML和面向agent建模语言CAMLE为例开展了实例研究,展示该了途径的可行性和实用性。该途径包括三个相互关联的部分:一致性约束的形式化定义技术,一致性约束的正确性证明方法和技术、一致性约束及一致性检查工具的有效性测试和评价的方法和技术。一致性约束是衡量模型一致性的标准,形式化定义的一致性约束是验证一致性约束、开发一致性检查工具和测试一致性检查工具的基础。在本文中我们把用来规约一致性约束的语言称为约束语言。本文提出从建模语言的抽象语法系统地导出基于一阶逻辑的约束语言的方法,并针对用GEBNF(Graphically Extended BNF)定义的文本形式的抽象语法和用UML元模型定义的抽象语法分别提出推导约束语言的技术。一致性约束必须以建模语言的语义为逻辑基础,而如何形式化地定义建模语言的语义并在此基础上证明一致性约束的正确性是个尚未解决的难题。本文提出用一阶逻辑对建模语言的描述语义进行形式化定义的方法。我们把模型的语义表达为描述被建模系统的一组一阶逻辑语句;把元模型的语义表达为所有模型都应满足的一组一阶语句,称之为模型的公理。通过逻辑推演,可以证明也表达为一阶语句的一致性约束与公理的逻辑一致性关系,从而验证一致性约束的正确性。对建模语言的语义的形式化使得我们可以通过证明表达模型语义的逻辑系统的逻辑一致性,直接验证模型的一致性。由于元模型的语义也表达为一阶逻辑系统,还可以通过逻辑推演验证元模型的一致性。我们实现了原型工具LAMBDES,该工具将UML的元模型和模型翻译成一阶系统,通过调用定理证明器对元模型和模型进行一致性检验,对一致性约束的正确性进行逻辑分析。以模型的形式化语义为基础,使用通用的逻辑推理系统直接对模型的一致性进行推理限于计算复杂性,实用性较低。因此,当前广泛使用的途径是把一致性约束实现为专用检验工具。此类工具的功能依赖于一致性约束的定义,因此,如何客观地评价一致性检查工具的有效性也是一个重要问题。本文提出一种称为数据变异测试的方法来测试一致性检查工具,评价其有效性。该方法通过设计一组变异算子来模拟建模中可能产生的错误。将变异算子作用在正确的模型上,可以得到大量的包含各种错误的变异模型,作为一致性检查工具的测试用例,从而可以对工具进行较全面和客观的测试和评估。对CAMLE一致性检查工具进行的实例研究展示了此方法的可行性和实用性。