基于SBOPN的UML模型的正确性验证

摘要

作为面向对象技术的标准语言,UML具有界面友好、易于表达、功能强大且普遍适用的特征,但是UML不是形式化的建模语言,缺乏精确的语义描述,因此难以在UML模型设计的早期阶段对模型进行分析验证.作为一种建模工具,Petri网既能对分布、并发的过程进行有效的形式化建模,又能对系统的结构和动态行为进行严密的数学分析和直观的计算机仿真,因此我们选择Petri网作为UML形式化方法.本文介绍了基于状态的对象Petri网(State-Based Object Petri Net,SBOPN),给出网的定义、引发规则和网的分析方法,并讨论其面向对象的特征.在此基础上我们利用基于状态的对象Petri网对UML进行形式化,给出UML模型中的状态图和协作图映射为基于状态的对象Petri网模型的机制和相应的实现算法,通过这些算法生成的Petri网模型既拥有其面向对象的特征,又可以利用Petri网的强大的分析工具对模型的进行分析验证,找出死锁状态,从而可以在模型设计的早期阶段实现对模型的正确性验证.利用该算法我们给出由微波炉系统和ATM机系统的UML模型映射为相应的基于状态的对象Petri网模型的实例,通过SBOPN的可达标识图,对飞船飞行控制系统的UML规范映射产生的基于状态的对象Petri网模型进行分析验证.在此基础上,给出基于SBOPN的UML模型验证工具原型.最后我们给出课题的下一步的研究方向.

目录

文摘

英文文摘

声明

1绪论

1.1课题的提出

1.2论文的整体安排

2 Petri网基础知识

2.1 Petri网及其应用简介

2.2 Petri网的基本概念

2.3 Petri网的基本性质

2.4 Petri网的基本分析方法

3基于状态的对象Petri网

3.1面向对象的Petri网介绍

3.2基于状态的对象Petri网

3.3基于状态的对象Petri网的分析方法

3.4基于状态的对象Petri网面向对象特征讨论

4基于SBOPN的UML模型的正确性验证

4.1 UML简介

4.2 UML向SBOPN映射的机制

4.3状态图简介

4.4 UML向SBOPN映射的实现

4.5基于SBOPN的UML模型的正确性验证

5结束语

5.1本文的主要工作

5.2进一步的工作

致谢

攻读硕士期间主要成果

参考文献