论文部分内容阅读
作为面向对象技术的标准语言，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模型验证工具原型。最后我们给出课题的下一步的研究方向。