关键词: UML2．0顺序图 UPPAAL 有穷自动机 时间自动机

Abstract:

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 seq  uence 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 dia gram, 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 con- straints 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

Key words: UML2.0 sequence diagram, UPPAAL, finite automata, timed automata