UML模型检测方法的研究

统一建模语言（UML）是设计和分析软件系统最常用的方法，如何保证UML模型满足某些特性是一个非常重要的问题，而模型检测是一种能够有效提高系统可靠性的自动化技术。研究了使用简单进程元语言解释器（SPIN）对UML模型进行检测的方法。首先对UML模型进行形式化描述，使用层次自动机来描述状态图，然后根据层次自动机的操作语义将状态图和类图的部分信息转化为SPIN的输入语言PROMELA，使用SPIN来验证模型是否满足给定的线性时序逻辑所描述的系统约束，通过LTL公式描述顺序图的方式来验证与状态图之间的一致性问题。项目组基于此方法还开发了一套模型检测工具UMLChecker。

Research of model checking UML

Unified Modeling Language (UML) is the most commonly used method in software system design and analysis, and how to verify that the UML model satisfies some properties is a very important issue. Model Checking is an efficient automatic technique for the improvement of system's reliability, and this paper is a research into how to check UML model through the Simple PROMELA Interpreter （SPIN） model-checker. After describing the UML model using formal method, we first used hierarchical automata to express statecharts diagram. In addition, we translated the statecharts and part of the class diagram into PROMELA based on the operational semantic of hierarchical automata, and verified the model by using Simple Promela Interpreter （SPIN） to test if it satisfied the LTL properties. We also verified the consistency between sequence diagram and statecharts diagram by using LTL formula to express sequence diagram. Finally, based on the method, we developed a model checker tool called UMLChecker.