基于Petri网的UML状态图的形式化验证

摘要

统一建模语言(UML，Unified Modeling Language)是一种非专利的可视化建模和规约语言。UML提供了开放的方法，用于系统说明、文档化、可视化构建面向对象的软件密集系统。然而UML并没有被赋予严格的形式化语义，而且对于动态模型仅仅只能描述而无法执行，这使得模型的验证成为一个难题。造成软件系统的许多缺陷在软件设计开发初期很难发现，导致开发成本的增加。相对而言，Petri网拥有丰富的理论基础，严格的形式化语义，而且是一种可执行的模型。本文着眼于两种模型的优势，将UML模型中的状态图转换为Petri网模型，进而通过对Petri网模型的分析验证达到确保原模型正确性和合理性的目的。
　　 本文首先针对UML和Petri网两种模型映射的国内外研究现状进行了分析和综述，基于相关的Petri网基础理论，在研究UML状态图向Petri网映射的方法中，以图模型为基础，提出了具体的映射规则，然后对映射规则的正确性进行了形式化证明，以确保二者语义上的等价性。在完成两种模型的映射基础上，设计开发了二者的自动转换工具，并通过一个实例讨论和分析了转换工具的工作流程合理性。
　　 本文以设计一个小型网络购物系统为实例，首先基于VP-UML设计系统的用例图、类图以及订单对象的状态图;然后针对订单对象状态图，采用本文所提出的方法，使用自动转换工具将其转为Petri网模型;最后根据Petri网理论对该模型进行相关的性质分析和行为验证。通过实例验证了映射方法的可行性和正确性。
　　 本文的主要工作和创新之处在于将UML模型以可执行模型的形式予以处理和展现，采取将UML模型映射为Petri网的方式，并从两个方面，即理论证明和实例验证，确保了映射规则和转换的正确性。网络购物系统的实例也证明该方法在软件设计与开发的实际工作中的适用性，显现出对于提高软件系统的正确性和可靠性的作用。

目录

声明

摘要

第1章 绪论

1．1 问题提出的背景与意义

1．2 国内外研究现状

1．2．1 Petri网的研究现状

1．2．2 UML形式化的研究现状

1．2．3 UML模型向Petri网转换的研究现状

1．3 本文的主要工作和创新点

1．4 本文的组织结构

第2章 Petri网理论基础

2．1 Petri网原理的基本概念

2．2 Petri网的性质

2．2．1 结构性质

2．2．2 动态性质

2．3 本章小结

第3章 UML状态图的Petri网建模

3．1 UML状态图概述

3．2 状态图到Petri网的映射规则

3．2．1 静态元素的映射原则

3．2．2 初始伪状态和终止状态

3．2．3 简单状态转换

3．2．4 分叉和结合

3．2．5 分支和合并

3．2．6 包含动作的状态转换

3．2．7 包含组合状态的状态图

3．2．8 包含历史状态的状态图

3．3 映射规则的正确性证明

3．4 本章小结

第4章 自动转换平台的搭建和实例验证

4．1 转换平台的搭建

4．1．1 状态图模型构建

4．1．2 模型转换阶段

4．1．3 模型分析验证阶段

4．2 实例分析和验证

4．2．1 系统概述

4．2．2 需求分析和设计用例

4．2．3 系统类图设计

4．2．4 状态图建模

4．2．5 数据库设计

4．3 状态图模型到Petri网模型的转换

4．4 Petri网模型性质验证

4．4．1 Petri网结构特性的一般分析方法

4．4．2 冲突检测

4．4．3 死锁检测

4．4．4 多种方法对比

4．5 本章小结

第5章 结束语

参考文献

致谢

攻读学位期间发表的学术论文