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