统一建模语言(Unified Modeling Language，UML)是一种描述能力强大且涵义直观的可视化建模语言，它提供多种图元从不同角度和应用层次刻画系统特性以及复杂的运行环境。基于UML的软件开发过程和建模环境已被工业界广泛接受，其中包括航天、国防、汽车等许多安全攸关领域。对UML模型进行正确性验证以判断设计规范是否满足目标需求成为一个关键问题。 模型检验(model checking)是一种重要的自动验证技术。UML Statecharts刻画了对象在其生命周期中的行为和状态变迁，在软件分析和设计建模过程中占有重要地位。本文提出了对UML Statecharts进行模型检验的方法。首先针对UML的特点对扩展层次自动机(Extended Hierarchical Automata，EHA)进行改进，以便能结构化地表示UML Statecharts，并给出相应的操作语义。通过寻找最大无冲突迁移集可以保证语义的正确性。研究了线性时态逻辑公式表达UML模型性质的特点和形式。在把根据EHA操作语义得到的标记迁移系统和表示性质的线性时态逻辑公式分别转换为Bǖchi自动机后，用基于自动机理论的模型检验方法验证UML Statecharts的正确性。 由于空间爆炸和语义的复杂性，对Statecharts进行模型检验受到软件规模和设计精化程度的制约。本文通过分析EHA中存在的层次、并发和同步等特征定义了一组依赖关系，对于由状态和迁移组成的切片准则，提出对EHA进行切片的算法。当按一定规则从被验证的性质中提取切片准则时，该算法能保证切片后的EHA与原模型对性质具有相同的满足性。切片方法删除了与待验证性质无关的层次和并发状态，缓解了空间爆炸问题，并且有助于模型的分析和理解。 对于并发多对象系统，可以使用UML协同图描述对象间的动态交互和链接关系。本文根据UML协同图和各对象的Statecharts，分别针对异步和同步模式提出对象合成的方法，以验证整个系统的性质。为缓解并发对象导致的状态爆炸问题，本文还研究了根据同步合成和结构间的模拟关系，对同步UML模型进行并发组合推理，使得有可能不必建立全局状态迁移图来验证系统。此外，根据Statecharts的特点把层次结构加入到组合验证的过程中，使得对实现的验证可以通过把系统的某些精化部分用更抽象的规范(通常有更小的状态空间)代替来进行。 我们设计并实现了一个UML模型检验工具UML-MC，可以对Rational Rose或I-Logix Rhapsody建立的Statecharts模型进行验证，并能在性质不满足时给出反例路径。此外，根据我们对UML测试和验证的研究成果，设计了一个基于UML的软件测试和验证环境的体系结构，并实现了原型系统。