随着软件的广泛应用，特别是软件在尖端领域的应用，软件的可靠性成为一个非常重要的问题。软件的可靠性主要取决于软件开发的方法与过程，同时，又取决于软件系统的测试与验证。UML是面向对象开发中一种可视化建模语言，已经成为事实上面向对象建模的标准。虽然UML表达丰富，但UML不是一种形式化的建模语言，其图形化的符号经常缺乏精确的语义。而且，传统的验证方法包括测试、模拟和仿真，它们均不能保证完全的错误覆盖。因此，对软件的UML模型进行形式化并对其进行形式化的验证非常必要。　　 本文首先提出了一种基于UML的软件模型检测方法，其主要步骤如下：　　 (1)将软件的UML模型转换为非形式化的基于XML的系统模型；　　 (2)从基于XML的系统模型中提取系统信息，对其进行形式化转换，得到系统的形式化的CTLMC语义模型；　　 (3)采用形式化验证工具CTLMC对形式化后的系统模型进行形式化验证；　　 (4)如果该模型不满足用户需求，CTLMC给出反例信息并将其以UML顺序图的形式显示表示。　　 接着，着重介绍了采用该方法进行模型检测所必须的两个转换工具(UML模型的形式化转换工具和反例信息的UML顺序图转换工具)的设计及实现。　　 然后，将本支所实现的这两个转换工具与本实验室开发的符号模型检测器"CTLMC"相结合，实现了一个基于UML的软件模型检测系统。　　 最后，通过两个实例对所实现的基于UML的软件模型检测系统进行验证。　　 根据本文提出的基于UML的软件模型检测方法所实现的基于UML的软件模型检测系统能够结合软件的UML类图、UML状态图和UML顺序图对软件的UML类图中单个类所对应的UML状态图中各个状态之间的状态迁移关系及其约束进行验证。采用本文提出的基于UML的软件模型检测方法，验证人员可以在对形式化方法知之甚少或一无所知的情况下，对软件的UML模型进行完全形式化的验证，而且，本文提出的基于UML的软件模型检测方法，可以在很大程度上降低软件系统的开发成本，提高软件系统的可靠性。