摘要：统一建模语言（UML）不能直接对所建立模型的正确性进行形式化验证。为解决上述问题，从UML模型的静态结构和动态行为2个方面分别提出结合行为时序逻辑（TLA）的模型形式化方法，在此基础上提出将UML模型转化为TLA＋的形式化描述方法，并用TLC工具形式化检测TLA＋描述的正确性。通过实例分析证明了该方法的有效性。