UML2．0顺序图的一种有穷自动机模型

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

An Finite Automata Model of the UML2.0 Sequence Diagram

In order to analyse and verify the UML2.0 sequence diagram model in the early stage of software development,a finite automata model of the UML2.0 sequence diagram is introduced in this paper.Firstly,the precise definitions of the UML sequence diagram in the forms of syntactics and semantics are presented.Then a finite automata is introduced to describe the events that every object participates in the scenario which is depicted by the sequence diagram,after that the automata is extended to describe the UML2.0 sequence diagram that contains combined fragments.Finally,the time modeling mechanism in the UML2.0 sequence diagram is analyzed,after that an algorithm is introduced to extract the timing constraints from the UML2.0 sequence diagram.All the work stated above lays the foundation for a further analysis and verification of the sequence diagram using UPPAAL.