论文部分内容阅读
摘 要：针对UML语言建立的自动取款机模型不能进行分析和验证的难题，本文采用UML-CPN方法对银行取款机进行建模，该方法结合UML和Petri网的优点，首先利用UML进行建模，然后再将其转化为Petri网进行模型的验证。实验结果表明，该方法能够较好的解决单一的UML或Petri网建模时无法进行验证的问题。
关键词：UML；Petri网；系统建模；ATM系统
引言
ATM(Automatic Teller Machine)自动取款机，是由计算机控制的自动出纳系统。它主要服务于活期储蓄，是实现客户自我服务的先进电子化设备。在我国，基本上所有的银行系统都有自己的ATM系统。
ATM系统的建模一般都使用UML语言，作为一种通用的可视化建模语言，UML虽然具有上述的多种优点，但是，采用图形化语言构筑的模型往往存在难以发现的模糊性或歧义性等问题将直接影响系统的安全性与可靠性［4］。而Petri网［6］是一种优秀的建模工具,它拥有多种分析方法和分析工具。使用Petri网不仅能利用其来规范语义，还能利用它强大的分析功能对网模型进行自动分析验证模型。因此，在系统设计中，综合运用Petri网和UML这两个建模工具，能够提高软件形式化描述的全面性、一致性、精确性和完整性，达到减少设计错误、提高系统可靠性、减少后期的测试与维护的成本、提高整个系统开发的效率的目的。本文基于UML-CPN建模方法，对自动银行取款机系统进行建模，较好的解决了单一的UML或Petri网建模时无法进行验证的问题。
1.基于UML的自动银行取款机系统建模
使用Rational Rose2003工具，对自动银行取款机系统进行建模。
1.1建立系统用例模型
建立用例视图通常包括三个步骤：
1.确定角色：结合ATM系统实际，确定了客户、银行人员和信用系统这三个角色。
2.创建用例：用例模型是系统和角色之间的对话，它表现系统提供的功能，是角色启动的，基于这样的考虑，ATM系统根据业务流程大致可以分为以下几个用例：（1）客户取款，（2）客户存款。（3）客户查询余额，（4）客户转账，（5）客户更改密码，（6）客户通过信用系统付款，（7）银行人员更改密码，（8）银行人员为ATM添加现金，（9）银行人员维护ATM硬件。
3.创建角色—用例关系图：在角色和用例之间存在关联关系，这种类型的关联关系通常涉及到角色和用例之间的通信关联关系。这个关系图直观显示了ATM系统使用用例与角色间的交互。由于用例关系图都比较简单和类似，在这里我们仅给出客户的用例关系图，如图1所示。
图中一共有六个用例：转账、存款、取款、付款、查询余额和修改密码。在这个关系图中，着重展示了客户能在ATM取款机前的业务用例。这与真实的情况基本相符，描述了客户能做什么。
1.2建立系统动态模型
动态模型包括活动图、状态图、时序图和协作图等。创建这些框图的目的是为了更好的了解业务流程。这些框图是对用例图的补充。
1.创建活动图：活动图展示了系统中功能流，可以在业务模型中显示业务工作流；可以在收集需求时显示一个使用用例的事件流。
如图2所示演示了“开户”活动的例子。从该图中可以看出：客户服务代表、信用部经理和客户三者发生了相互的关系。
2.创建协作图：协作图只对相互间有交互作用的对象和这些对象间的关系建模，而忽略其他对象和关系。它可以被视为对象图的扩展，但它除了展现出对象间的关联外，还显示了对象间的消息传递。如图3所示，给出了使用Rose2003所绘制的UML取款的协作图。
3.创建状态图：状态图展示了一个特定对象的所有可能状态以及由于各种ATM件的发生而引起的状态间的转移。状态图对于接口、类或协作的行为建模尤为重要，可以用它描述用例的生命周期。图4描述了顾客在ATM机上进行操作会经历的几种状态，及各种状态之间转换的条件。因为是简化了的例子，所以除了等待顾客插入磁卡的起始状态和结束服务的终止状态，顾客会处于输入密码、选择服务类型、存款及取款四种状态。
插入磁卡后进入输密码状态，当密码输入正确时进入选择服务类型状态，当输入密码不正确时，停留在原状态。进入选择服务类型后根据选择的不同，顾客可进入存款和取款状态。存款、取款结束后，顾客既可以选择结束服务到最终状态，也可以选择继续服务回到选择服务类型状态。
通过状态图我们可以无歧义的了解各个活动角色是如何在不同状况下转换的，转换的条件是什么，是否会出现死锁现象，是否有条件没考虑周全，是否有状态无法达到。状态图4以帮助我们发现问题，并及时改正。
2.系统模型转换及验证
在UML模型中，状态图描述了对象在事件驱动下状态转移的流程,反映了一个对象的生命期内的行为，因此，可从状态图中获取信息，构造部分着色Petri 网。得到部分CPN网后,将对部分CPN模型按照一定的原则连接起来，形成整个系统的CPN模型。下面就给出其中一个UML状态图转换后的Petri网模型以示说明。（图5所示的就是由图4转换而来的Petri网模型。）
对于映射得到的Petri网模型，一方面可以利用Petri网的各种分析方法对其进行严格的定性分析和验证，主要包括：分析模型的活性、有界性、可达性、系统是否存在冲突、死锁等。另一方面，也可以通过对Petri网模型的计算仿真，在系统投入运行之前分析其生产周期、生产成本等性能参数以发现可能存在的问题，然后根据分析和仿真的结果，进一步的修正和改进系统模型。通过模拟我们可以发现问题，但并不能保证不会出现所有我们并不期望的行为。
转换为Petri网时，需要预定义变量部分。CPN ML在CPN Tools中对应的定义如下所示：
colset UNIT=unit;
colset INT=int;
使用CPN Tools分析着色Petri网包括语法校验、网络的仿真和状态空间分析。进行语法校验时，CPN Tools会自动检测所创建或者测载入的网络。我们可以通过颜色指示看到检测进行了多久。 颜色指示显示在索引中颜色所属页面的名称的下划线处。 如果页面在一个组合体中打开, 颜色也显示在最上面页面的页面标签下，和颜色所属的CP-net元素上。当载入一个网络时，语法检测需要2分钟完成。 在这个阶段，网络元素将会改变光环的颜色从橙色到黄色然后就是没有光环(或者是红色，如果出现错误的话)。当网络通过语法检测后，将仿真工具从索引拖出到工作空间就可以进行仿真了。其工具栏如图6所示。当仿真程序运行时，将会显示如下的仿真反馈信息：在库所旁会显示库所的当前标识；授权变迁的周围会出现绿色的光环而且授权变迁所在的页面下会出现绿色的下划线 (显示在索引处和页面tabs处)；步数和时间显示在索引中正被仿真的网络下。还可以使用CPN Tools的状态空间工具对模型进行仿真。其状态空间工具栏如图7所示。图8显示的是图5的状态空间结果。
通过分析可知，该图存在死锁问题。即当用户忘记银行卡的密码，或者银行卡不是该用户的，而用户一直尝试输入密码，若密码一直错误，则该系统就一直处在输入密码状态。由此，我们对该状态图的UML模型进行改进以解决该问题。我们规定：若输入三次密码均不正确，则系统自动退出。改进后的状态图如图9所示。再次对该图进行上述验证，则发现该图是正确的。
可达树用以描述Petri网的可达集，它不仅和Petri网的结构有关，还和Petri网的初始标识有关。通过分析Petri网的可达树，可以了解Petri网的许多重要的如有界性、可达性、死锁等性质。可达树已被证明是一种有效的分析方法。对于一般的嵌入式系统设计而言，利用模拟分析的方法基本已经足够了。
上述的例子说明了UML模型到Petri网模型的转换及验证。而实际的情况可能会更复杂，但实验仍能证明UML-Petri集成建模方法对于嵌入式系统的开发确实是有效的。
3.结束语
事实表明，单一使用UML进行建模难以实现对所建模型的验证问题。本文采用UML-CPN建模方法。利用该方法对自动取款机系统进行建模，既可以弥补形式化程度较低、缺乏精确的语义描述、难以在模型设计的早期阶段进行分析与验证等不足，又可以降低Petri网作为形式化数学工具的使用难度，并为用Petri网相关工具对模型进行正确性验证提供了一种途径。对其它系统的建模有一定的指导意义。
［参考文献］
［1］郭峰,姚淑珍.基于Petri网的UML状态图的形式化模型［J］.北京:航空航天大学学报.2007,33(2):248-252.
［2］谢彦辉,姚淑珍,郭峰.顺序图至Petri网转化方法的研究与实现［J］.计算机工程.2006,32(6):260-262.
［3］孙莹,蒋波,王赫.UML通信图和Petri网转换方法的研究［J］.系统仿真学报.2007,19（1）：104-105.
［4］徐宝文,周毓明,卢红敏.UML与软件建模［M］.北京:清华大学出版社,2006:23-26.
［5］陈涵生,郑明华.基于UML的面向对象建模技术［M］.北京：科学出版社,2006:58-62.
(作者单位：三门峡职业技术学院 信息工程系，河南 三门峡 472000)
关键词：UML；Petri网；系统建模；ATM系统
引言
ATM(Automatic Teller Machine)自动取款机，是由计算机控制的自动出纳系统。它主要服务于活期储蓄，是实现客户自我服务的先进电子化设备。在我国，基本上所有的银行系统都有自己的ATM系统。
ATM系统的建模一般都使用UML语言，作为一种通用的可视化建模语言，UML虽然具有上述的多种优点，但是，采用图形化语言构筑的模型往往存在难以发现的模糊性或歧义性等问题将直接影响系统的安全性与可靠性［4］。而Petri网［6］是一种优秀的建模工具,它拥有多种分析方法和分析工具。使用Petri网不仅能利用其来规范语义，还能利用它强大的分析功能对网模型进行自动分析验证模型。因此，在系统设计中，综合运用Petri网和UML这两个建模工具，能够提高软件形式化描述的全面性、一致性、精确性和完整性，达到减少设计错误、提高系统可靠性、减少后期的测试与维护的成本、提高整个系统开发的效率的目的。本文基于UML-CPN建模方法，对自动银行取款机系统进行建模，较好的解决了单一的UML或Petri网建模时无法进行验证的问题。
1.基于UML的自动银行取款机系统建模
使用Rational Rose2003工具，对自动银行取款机系统进行建模。
1.1建立系统用例模型
建立用例视图通常包括三个步骤：
1.确定角色：结合ATM系统实际，确定了客户、银行人员和信用系统这三个角色。
2.创建用例：用例模型是系统和角色之间的对话，它表现系统提供的功能，是角色启动的，基于这样的考虑，ATM系统根据业务流程大致可以分为以下几个用例：（1）客户取款，（2）客户存款。（3）客户查询余额，（4）客户转账，（5）客户更改密码，（6）客户通过信用系统付款，（7）银行人员更改密码，（8）银行人员为ATM添加现金，（9）银行人员维护ATM硬件。
3.创建角色—用例关系图：在角色和用例之间存在关联关系，这种类型的关联关系通常涉及到角色和用例之间的通信关联关系。这个关系图直观显示了ATM系统使用用例与角色间的交互。由于用例关系图都比较简单和类似，在这里我们仅给出客户的用例关系图，如图1所示。
图中一共有六个用例：转账、存款、取款、付款、查询余额和修改密码。在这个关系图中，着重展示了客户能在ATM取款机前的业务用例。这与真实的情况基本相符，描述了客户能做什么。
1.2建立系统动态模型
动态模型包括活动图、状态图、时序图和协作图等。创建这些框图的目的是为了更好的了解业务流程。这些框图是对用例图的补充。
1.创建活动图：活动图展示了系统中功能流，可以在业务模型中显示业务工作流；可以在收集需求时显示一个使用用例的事件流。
如图2所示演示了“开户”活动的例子。从该图中可以看出：客户服务代表、信用部经理和客户三者发生了相互的关系。
2.创建协作图：协作图只对相互间有交互作用的对象和这些对象间的关系建模，而忽略其他对象和关系。它可以被视为对象图的扩展，但它除了展现出对象间的关联外，还显示了对象间的消息传递。如图3所示，给出了使用Rose2003所绘制的UML取款的协作图。
3.创建状态图：状态图展示了一个特定对象的所有可能状态以及由于各种ATM件的发生而引起的状态间的转移。状态图对于接口、类或协作的行为建模尤为重要，可以用它描述用例的生命周期。图4描述了顾客在ATM机上进行操作会经历的几种状态，及各种状态之间转换的条件。因为是简化了的例子，所以除了等待顾客插入磁卡的起始状态和结束服务的终止状态，顾客会处于输入密码、选择服务类型、存款及取款四种状态。
插入磁卡后进入输密码状态，当密码输入正确时进入选择服务类型状态，当输入密码不正确时，停留在原状态。进入选择服务类型后根据选择的不同，顾客可进入存款和取款状态。存款、取款结束后，顾客既可以选择结束服务到最终状态，也可以选择继续服务回到选择服务类型状态。
通过状态图我们可以无歧义的了解各个活动角色是如何在不同状况下转换的，转换的条件是什么，是否会出现死锁现象，是否有条件没考虑周全，是否有状态无法达到。状态图4以帮助我们发现问题，并及时改正。
2.系统模型转换及验证
在UML模型中，状态图描述了对象在事件驱动下状态转移的流程,反映了一个对象的生命期内的行为，因此，可从状态图中获取信息，构造部分着色Petri 网。得到部分CPN网后,将对部分CPN模型按照一定的原则连接起来，形成整个系统的CPN模型。下面就给出其中一个UML状态图转换后的Petri网模型以示说明。（图5所示的就是由图4转换而来的Petri网模型。）
对于映射得到的Petri网模型，一方面可以利用Petri网的各种分析方法对其进行严格的定性分析和验证，主要包括：分析模型的活性、有界性、可达性、系统是否存在冲突、死锁等。另一方面，也可以通过对Petri网模型的计算仿真，在系统投入运行之前分析其生产周期、生产成本等性能参数以发现可能存在的问题，然后根据分析和仿真的结果，进一步的修正和改进系统模型。通过模拟我们可以发现问题，但并不能保证不会出现所有我们并不期望的行为。
转换为Petri网时，需要预定义变量部分。CPN ML在CPN Tools中对应的定义如下所示：
colset UNIT=unit;
colset INT=int;
使用CPN Tools分析着色Petri网包括语法校验、网络的仿真和状态空间分析。进行语法校验时，CPN Tools会自动检测所创建或者测载入的网络。我们可以通过颜色指示看到检测进行了多久。 颜色指示显示在索引中颜色所属页面的名称的下划线处。 如果页面在一个组合体中打开, 颜色也显示在最上面页面的页面标签下，和颜色所属的CP-net元素上。当载入一个网络时，语法检测需要2分钟完成。 在这个阶段，网络元素将会改变光环的颜色从橙色到黄色然后就是没有光环(或者是红色，如果出现错误的话)。当网络通过语法检测后，将仿真工具从索引拖出到工作空间就可以进行仿真了。其工具栏如图6所示。当仿真程序运行时，将会显示如下的仿真反馈信息：在库所旁会显示库所的当前标识；授权变迁的周围会出现绿色的光环而且授权变迁所在的页面下会出现绿色的下划线 (显示在索引处和页面tabs处)；步数和时间显示在索引中正被仿真的网络下。还可以使用CPN Tools的状态空间工具对模型进行仿真。其状态空间工具栏如图7所示。图8显示的是图5的状态空间结果。
通过分析可知，该图存在死锁问题。即当用户忘记银行卡的密码，或者银行卡不是该用户的，而用户一直尝试输入密码，若密码一直错误，则该系统就一直处在输入密码状态。由此，我们对该状态图的UML模型进行改进以解决该问题。我们规定：若输入三次密码均不正确，则系统自动退出。改进后的状态图如图9所示。再次对该图进行上述验证，则发现该图是正确的。
可达树用以描述Petri网的可达集，它不仅和Petri网的结构有关，还和Petri网的初始标识有关。通过分析Petri网的可达树，可以了解Petri网的许多重要的如有界性、可达性、死锁等性质。可达树已被证明是一种有效的分析方法。对于一般的嵌入式系统设计而言，利用模拟分析的方法基本已经足够了。
上述的例子说明了UML模型到Petri网模型的转换及验证。而实际的情况可能会更复杂，但实验仍能证明UML-Petri集成建模方法对于嵌入式系统的开发确实是有效的。
3.结束语
事实表明，单一使用UML进行建模难以实现对所建模型的验证问题。本文采用UML-CPN建模方法。利用该方法对自动取款机系统进行建模，既可以弥补形式化程度较低、缺乏精确的语义描述、难以在模型设计的早期阶段进行分析与验证等不足，又可以降低Petri网作为形式化数学工具的使用难度，并为用Petri网相关工具对模型进行正确性验证提供了一种途径。对其它系统的建模有一定的指导意义。
［参考文献］
［1］郭峰,姚淑珍.基于Petri网的UML状态图的形式化模型［J］.北京:航空航天大学学报.2007,33(2):248-252.
［2］谢彦辉,姚淑珍,郭峰.顺序图至Petri网转化方法的研究与实现［J］.计算机工程.2006,32(6):260-262.
［3］孙莹,蒋波,王赫.UML通信图和Petri网转换方法的研究［J］.系统仿真学报.2007,19（1）：104-105.
［4］徐宝文,周毓明,卢红敏.UML与软件建模［M］.北京:清华大学出版社,2006:23-26.
［5］陈涵生,郑明华.基于UML的面向对象建模技术［M］.北京：科学出版社,2006:58-62.
(作者单位：三门峡职业技术学院 信息工程系，河南 三门峡 472000)