统一建模语言UML是在多种面向对象建模方法联合的基础上发展而来的，由于其概念明确，图形结构清晰，建模方法简洁，易于掌握和使用，且不依赖于特定的软件开发过程，于1997年被对象管理组织OMG采纳为建模语言规范，并逐渐成为了实际的工业标准。但是UML是半形式化的。UML的语法结构采用了形式化的规约，语义部分则是用自然语言描述的。这种共存的形式导致uML语义的不一致性，容易产生歧义，使得相关工具对该语言的支持只能限制在语法是否正确的检查层次上，而无法对所定义模型的正确性和一致性进行严格的分析和检验。这可能会导致一个含有错误设计的模型在软件设计和开发的过程中被使用，从而降低软件开发的效率和质量，甚至可能会造成整个软件项目的失败。形式化方法则是基于严格的数学推理的方法，是一种精确的、无二义的形式规约准则，为模型的准确理解提供严格的数学基础，这对提高软件的自动代码生成和进行可靠的软件开发有着非常重要的意义。本文以uML顺序图为研究对象，采用描述逻辑和计算树逻辑相结合的方法，对uML顺序图进行了形式化研究，提高uML顺序图语义的精确性。本文首先在总结前人进行UML形式化研究的基础上，比较了各种形式化方法的异同点，分析了其中一些方法的不足和缺陷，同时详细比较了uML和描述逻辑的异同点。其次，针对描述逻辑在表示动态和时态知识的不足和计算树逻辑在表示静态知识的缺陷以及二者存在互补的特点，采用了将二者进行结合的形式化描述方法，并对该形式化方法进行了详细的叙述和说明。最后，利用该形式化方法对UML的顺序图进行形式化研究，验证了该形式化方法的可行性，并对UML顺序图的静态和动态语义进行了检测。