摘要：为了在软件开发早期阶段对UML2．0顺序图模型进行分析和验证，本文给出了UML2．0顺序图的一种有穷自动机模型。首先给出了顺序图在语法和语义上的形式化描述，然后提出了一种使有穷自动机来描述每个对象在顺序图描述的场景中所参与的事件序列的方法，并将该方法扩展到带有组合片段的UML2．0顺序图，最后分析了UML2．0顺序图中的时间建模机制，设计了从UML2．0顺序图中提取时间约束的算法。以上工作为使用模型检测工具UPPAAL对顺序图模型进行进一步的分析与验证奠定了基础。

关键词：uppaal 有穷自动机 时间自动机 

单位：苏州大学计算机科学与技术学院 江苏苏州215006 暨南大学深圳旅游学院 深圳518053