基于Petri网的UML形式化研究

论文摘要

面向对象技术的发展,出现了众多的面向对象的建模语言,其中统一建模语言UML作为一种定义良好、功能强大的图形化建模语言得到广泛的运用。UML溶入了软件工程领域的新思想和新技术,支持从软件需求分析到软件交付使用的软件开发全过程,已经成为实际上的工业标准。然而,随着软件规模和复杂程度的不断提高,系统建模的要求也不断提高。复杂系统建模需要严格的形式化分析和验证才能保证系统的正确性,而UML的语法采用了形式化的规约,但是语义部分使用自然语言描述的,缺乏准确性,难以对建立的模型进行动态的分析和验证。随着对软件质量要求的提高,UML形式化研究越来越受到重视。本文针对UML是图形化描述的特点,选择Petri网系统作为形式化规范,避免了直接使用形式化规范的方法用于建模比较困难的局限性。Petri网和UML一样也是图形化的建模工具,因此能够更加容易地结合两者的优点。与UML相比作为一种系统模型的Petri网,它既可以展示系统的结构,又可以描述系统的动态行为。Petri网图形表示很直观,具有坚实、严格的数学基础,拥有许多成熟的分析方法可以直接用于分析模型的性能。本文改进了UML状态图和UML顺序图转换为Petri网的方法,对于UML顺序图,扩展了其表述能力,引入并发、同步、选择三种特殊的消息传递机制,更好地描述了系统的运行。本文对于建立的形式化Petri网模型使用构造可达树算法,分析Petri网模型的可达性、安全性、活性等多种动态特征,来改善UML模型,提高软件的质量。改进了构造可达树算法,定义了数据结构,减少了存储空间和计算复杂度,提高了分析Petri网模型的效率。本文详细描述了安徽省政策性农业保险气象服务业务系统的UML形式化建模和分析过程,得到了保险气象评价系统的形式化Petri模型,并加以分析验证。开发了使用可达树算法的Petri网特性的自动化分析工具。

论文目录

• 摘要
• Abstract
• 第一章 绪论
• 1.1 UML的发展现状和不足之处
• 1.2 UML形式化方法分类
• 1.3 课题的研究内容、方法以及意义
• 1.4 论文的组织
• 第二章 UML和Petri网技术
• 2.1 UML基本内容
• 2.1.1 UML的基本定义
• 2.1.2 UML的组成
• 2.2 Petri网主要知识
• 2.2.1 Petri网的相关定义
• 2.2.2 Petri网的动态性质
• 2.2.3 Petri网的分析方法
• 2.3 高级Petri网
• 2.4 小结
• 第三章 UML的Petri网形式化建模
• 3.1 UML状态图转换为对象Petri子网
• 3.1.1 复合状态转换为简单状态
• 3.1.2 简单状态图映射为OPM模型
• 3.2 UML顺序图的Petri网建模
• 3.2.1 UML顺序图的扩展
• 3.2.2 扩展的UML顺序图转换为Petri网模型
• 3.3 小结
• 第四章 形式化模型的验证分析算法与实现
• 4.1 可达树算法改进与实现
• 4.2 利用可达树分析动态行为特征
• 4.3 小结
• 第五章 UML形式化建模应用案例
• 5.1 保险气象评价系统的UML顺序图和状态图形式化模型
• 5.2 保险气象评价系统的形式化模型的验证与分析工具的实现
• 5.3 小结
• 第六章 结论与展望
• 参考文献
• 附录
• 致谢
• 攻读学位期间参加的科研工作和发表的学术论文