现代信息系统作为一种典型的复杂系统其规模越来越大，用户需求日趋复杂，项目失败率居高不下，能否在需求分析阶段建立语义正确的UML/OCL模式成为项目开发的关键因素。语义不一致性的检测是保证UML/OCL模式语义正确性的主要手段，目前的研究现状表明针对OCL约束的语义不一致性检测是研究中的薄弱环节。本文针对UML类图和OCL不变式组成的UML/OCL模式，研究基于OWL2DL本体的OCL不变式语义不一致性自动检测方法。依照该方法，可开发出相应软件工具，在需求分析阶段就能自动检测出OCL不变式语义不一致性，有效地保证了UML/OCL模式对后续的设计与实现环节进行正确指导，很大程度上提高了最终信息系统的质量。本文研究工作由重庆市自然科学基金重点项目资助，其研究成果具有重要的理论意义和实用价值。本文取得了以下三个方面的创新成果：①基于一阶谓词逻辑的ATuo2方法的形式化框架。本文提出了基于元模型的ATuo2方法，由于UML/OCL元模型采用了非形式化定义方式，而OWL2DL本体元模型虽然是形式化定义的，但是研究域范围和UML/OCL元模型完全不同，为了保证映射规则的整体性、系统性和精确性，通过对UML/OCL元模型和OWL2DL本体元模型的深入研究，定义出这两种元模型在统一域范围内基于一阶谓词逻辑的ATuo2方法的形式化框架，并给出在该形式化框架下映射规则的定义方式。②OCL表达式到OWL2DL类表达式的语义保持的自动转换方法。基于抽象语法树提出了OCL表达式到OWL2DL类表达式语义保持的转换流程，基于ATuo2方法的形式化框架分别给出4种OCL表达式抽象语法到OWL2DL本体元模型的映射规则。考虑到OWL采用开放世界假设，本文研究了如何使用封闭公理来实现OCL关系表达式语义保持的转换。由于OWL2DL不提供条件表达构子，本文应用本体设计模式来模拟If-then-else-endif语句的语义，实现了OCL条件表达式语义保持的转换。依照该方法，用户不仅可方便地将OCL不变式人工转换成OWL2DL公理，而且还可以开发相应的软件工具，实现机器自动转换。③基于描述逻辑调试推理的OCL不变式最小语义不一致性检测方法。本文引入OCL不变式最小语义不一致性的概念，并通过形式化定义讨论了它的基本性质。为能够在描述逻辑推理基础上检测出OCL不变式最小语义不一致性，本文将OCL不变式最小语义不一致性在OWL2DL本体下的表达形式定义为OWL2DL本体的概念不可满足性原因，将检测OCL不变式最小语义不一致性转换为查找OWL2DL概念不可满足的原因，并且基于描述逻辑调试推理设计出OCL不变式最小语义不一致性检测算法。最后，对全文的研究工作进行总结，指出了本文工作存在的不足以及今后工作中进一步研究的方向。