在基于UML的软件开发过程中，各种UML图形从不同侧面描绘着所开发的软件系统，这些图形之间存在着信息的重叠，从而导致UML模型的一致性问题。UML模型的一致性问题也是建模过程中一个重要并且需要解决的问题。 KeY Tool是一个支持形式化规范和代码验证的工具，该工具基于动态逻辑对程序和形式化规范进行分析和验证，然而该工具并不支持在设计阶段对UML模型进行一致性检验。作为KeY Fool的基础，动态逻辑不仅具备描述程序设计语言的能力，而且能够描述UML/OCL中的动态概念。因此，研究利用动态逻辑来解决UML 模型的一致性问题具有理论意义和应用价值。 本论文首先对UML模型存在的一致性问题进行综述，在此基础上深入分析已有的方法，即Greg提出的利用动态逻辑来检验UML模型一致性的方法中存在的问题。Greg的方法只针对某一特定简单的UML模型进行设计，而本论文从一般UML模型的基本要素出发来分析模型转换的方法，解决了原有方法中存在的一些问题。并且，原有方法只支持类图、顺序图和状态图的检验，本论文对该方法进行扩充，增加了OCL规范与其他UML图形之间的一致性检验。 通过案例分析表明，改进和扩充后的方法不但能检验出更多UML图形之间的一致性问题，而且能检验出OCL约束与其他UML图形之间的一致性问题。