统一建模语言 UML是一种通用的图形化建模语言， 在面向对象系统的分析和设计中， 它已成为了事实上的工业标准。但 UML不是形式化的建模语言， 缺乏精确的、 形式化的语义， 因此阻碍了它的进一步发展。线性时序逻辑是并发或反应式程序动态语义的一种形式化描述语言， 它适合用来精确地表示模型的动态语义。本文定义了顺图的形式化语法， 采用线性时序逻辑给出了顺序图的语义描述， 并通过实例分析， 对模型的某条性质进行了证明，为模型做进一步分析和验证提供了基础。