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

摘要：

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

关键词：UML2.0顺序图、UPPAAL、有穷自动机、时间自动机

所属期刊栏目：30

分类号：TP311(计算技术、计算机技术)

资助基金：江苏省高校自然科学研究项目08KJB520010;重庆市自然科学基金资助项目2006BB2259

在线出版日期：2009-02-16（万方平台首次上网日期，不代表论文的发表时间）

页数：共5页

页码：118-121,141