形式化方法借助数学方法为系统的说明、开发和验证提供了一个框架，有利于发现目标软件系统需求中的不一致性、不完整性等问题。 统一建模语言UML是当前软件工程领域的研究热点，它提供了多种图元从不同角度和应用层次刻画系统的特性以及复杂的运行环境，其中也包括了大量的具有模糊、稀疏语义的标准元素。在UML规范中，静态语义是用OCL语言和自然语言描述的，而动态语义却基本上是用自然语言来描述的，因此UML缺乏一个严格的动态语义定义。UML序列图反映了系统中并发对象之间的消息交互及顺序，在软件建模中占有重要地位，所以UML序列图的形式语义研究对于增进UML的清晰性、等价性、一致性和可扩展性是十分有意义的。 本文针对UML半形式化的特点主要研究如何将统一建模语言UML与形式化方法相结合，提高UML语义的准确性，实现对模型进行语义分析和一致性检验，从而可以在软件开发的早期发现系统描述的不一致或不完整，进而提高软件的可靠性和质量。本文在全面研究形式化方法的产生、作用、分类以及发展的基础上最终确定了以指称语义学对UML序列图进行形式规范；通过进一步地深入研究指称语义学以及UML序列图，本文采用指称语义学方法分别定义了序列图的语法域、抽象语法、语义域以及语义函数，从序列图的各个语法对象的功能的角度对序列图进行了形式化描述；在对序列图进行形式规范的基础上，采用了可扩展的标记语言XML文档格式对UML序列图进行存储；通过对序列图的消息时序关系以及对象状态的分析，提出了对具有全序关系的UML序列图进行语义处理的算法；在算法实现部分，使用了JAVA语言，在获取XML文档的DOM模型的基础上，利用了XML4J解析器以及JAVA语言中的集合，对XML文档的DOM模型进行了解析，通过比较XML文档中记录的对象的相邻消息的后置状态与前置状态是否一致来确定消息序列的正确性，从而实现了对UML序列图的语义处理。 本文最后提供了一个具体实例，通过对描述一个具体场景的序列图的语义进行检验，发现了序列图中存在的语义错误，从而发现了系统分析阶段描述的不一致性，由此证明了本文提出的方法具有有效性以及实用性。