刘丰年

摘 要： 针对UML建立ATM自动取款机系统模型时缺乏精确的语义描述、无法进行形式化的分析和验证等缺点，本文提出了一种基于UML-Petri网的ATM自动取款机建模方法。该方法首先采用UML对ATM自动取款机系统进行建模，然后参照一定的映像规则将UML模型转换为Petri网模型进行验证和分析，最后根据分析结果对UML模型进行修正和优化。结果表明，该方法合理将面向对象的UML建模方法和形式化的Petri网建模方法有效结合，取长补短，提高了系统的正确性、可靠性和开发效率，具有一定的理论价值和实际应用价值。

关键词： ATM自动取款机； 系统建模； UML-Petri网

中图分类号： TP 311.52 文献标志码： A 文章编号： 1671-2153（2016）01-0091-04

1 问题提出

伴随着金融业和电子网络技术的迅速发展，对ATM自动取款机系统提出了越来越高的要求。传统的ATM自动取款机系统主要采用面向对象的UML建模方法，但该方法缺乏精确的语义描述，无法对其建立的模型进行形式化的分析和验证，无法确保系统的安全性和可靠性。因此亟需一种新的嵌入式系统建模方法，既能方便开发人员使用，又能实现模型的分析和验证，目前，综合的系统建模方法已成为嵌入式系统建模的核心问题，备受关注。

本文根据目前ATM自动取款机运行中存在的问题，在对UML和Petri网建模方法优缺点进行认真分析的基础上，提出了一种基于UML-Petri网的ATM自动取款机建模方法，该方法首先采用UML对ATM自动取款机系统进行建模，然后参照一定的规则将UML模型转换为Petri网模型进行验证和分析，最后根据分析结果对UML模型进行修正和优化。……