近年来，软件规模的不断扩大，复杂度不断增加，如何提高软件开发效率，保证软件的质量成为软件工业界的关键性问题。统一面向对象建模技术为提高大规模软件开发的效率与质量带来了希望，为软件开发自动化奠定了基础。统一面向对象软件建模语言UML以其图形化的表达及对软件设计提供各种各样的支持而迅速成为软件业界的标准。开发人员可以使用多种角度对系统进行建模，但是不同视图模型可能存在信息冗余，可能导致视图不一致性等问题。因此，对UML进行形式化描述与研究，给出UML准确的形式化定义，可以提高该语言的准确性、扩展性和一致性。 UML顺序图常用于描述并发系统的设计需求，着重体现对象之间消息传递的时间顺序，因此，用一个适当的时序逻辑描述语言来给出它的语义是可行的。XYZ/E是一种可执行的线性时序逻辑语言，既可描述系统的动态行为又可表示程序性质，对顺序图进行形式化规约后，可在统一的时序逻辑框架下分析顺序图的性质。论文给出了一个改进的顺序图语法定义，同时对基于XYZ/E时序逻辑语言的UML顺序图语义进行了深入研究，针对存在的问题，根据给出的语法定义，提出了新的解决方案，更加精确地描述了顺序图的语义。 本文主要是对具有多种逻辑语义的顺序图提出语义分析方法，为复杂层次结构的状态图引入自动机，应用自动机算法得到自动机树，同时制定了新的顺序图与状态图的一致性检测准则，用模型检验工具SPIN对顺序图与其相关的状态图进行一致性检测。