摘要： 在模型驱动开发的场景下，保证UML 模型的一致性具有重要意义，但目前大多数UML/MDA 工具仅提供了有限支持。该文提出了一种基于代数重写逻辑的UML 模型一致性检查的方法。首先定义了基于两级代数规范的实施构架以分别检查UML 模型的设计时和运行时语义一致性，其次定义了检查包括类图、状态机图和顺序图在内的多图一致性的重写规则。该方法为保持面向可执行的UML 模型的一致性提供了有效支持。

关键词: 模型检查；重写逻辑；代数规范；UML

Abstract: Keeping the consistency of a UML model is very important under the model-driven development scene. Currently only limited support is provided by most UML or MDA tools. This paper proposes a method of checking the consistency of a UML model based on the algebraic rewriting logic. First, an implementation architecture based on two-level algebraic specifications is defined to check a UML model's semantic consistency of design-time and run-time, then rewrite rules are defined to check the consistency of multi-diagrams which include class diagrams,state machine diagrams and sequence diagrams, etc. The method can provide an effective support for keeping the consistency of executable-oriented UML models.

Key words: Model checking; Rewriting logic; Algebraic specification; UML