UML是一个通用的可视化的对象建模语言，经过了近十多年的发展和完善，在软件工业中已成为占支配地位的建模语言。UML在对系统进行建模时，由于其缺少分析系统结构的准确语义，且UML内部的多视角视图之间也存在不一致性的情况。因此，对UML模型的正确性难于保证，进而也限制了UML模型的有效性。　　 形式化方法是软件开发过程中用于分析、设计及实现系统的软件工程方法，是软件规格和验证的方法。形式化方法具有清晰、精确、抽象、简明、规范地验证软件系统及其性质的能力，能帮助发现其它方法不容易发现的系统描述的不一致等问题，有助于增加开发人员对系统的理解，能够极大地提高软件的安全性和可靠性。　　 针对形式化方法与可视化方法的优缺点，本文基于形式化方法与可视化UML相结合的建模思想，设计了一套从UML模型到Promela模型的转换规则，用时态逻辑LTL刻画系统模型性质，开发了由UML模型自动生成Promela代码的转换工具。在转换工具中通过调用SPIN自动验证Promela代码，来验证UML模型的正确性，若UML模型与刻画的性质不一致，SPIN将给出违反系统性质的反例。通过转换工具对实例进行验证，实验结果表明此工具的有效性。