摘要： 用户可使用UML从不同角度对系统进行建模，但不同视图间存在信息冗余，可能导致视图不一致问题。该文针对具有多种逻辑语义的顺序图提出分析方法，为复杂层次结构的状态图引入有限状态自动机，利用自动机分解算法得到自动机树。制定新的顺序图和状态图一致性检查准则和Promela代码结构，用模型检验工具SPIN进行顺序图及其相关状态图的一致性检验。

关键词: 统一建模语言, 模型检验, 有限状态自动机

Abstract: UML can be used to accomplish the system modeling from different views. There are information redundancy in different views, so that the views may be inconsistent. This paper proposes an approach to analyze sequence diagram which has many different logical semantics. To deal with the hierarchy structure of statechart, finite state automata is used in this paper, and an automata decomposition algorithm is proposed to get an automata tree. A new model consistency criterion of sequence diagram and statechart, as well as a new structure of Promela is proposed. Model consistency is checked between sequence diagram and statechart with the model checker SPIN.

Key words: Unified Modeling Language(UML), model check, finite state automata

中图分类号: 

• TN911.73