随着计算机软件应用的深入，人们对软件的质量和可靠性提出了更高的要求，通常采用系统建模和软件测试来保障。模型检测作为一种形式化的验证技术，有着自动化和提供反例等诸多优点。因此，本文的主要研究工作是利用模型检测技术来实现统一建模语言UML一致性检验和测试用例自动生成，从而来保证软件的高可靠性。UML是一种描述能力强大且涵义直观的可视化建模语言，然而由UML得到的表示系统多个方面的模型之间存在着一定的信息冗余和相互交织，从而可能会产生不一致性问题。本文提出了一套UML2.0中顺序图和状态图到SMV语言的转换准则，解决了顺序图中的组合片段和异步消息等特性。把状态图和顺序图分别表示为SMV语言模型和CTL时序逻辑，使用模型检测工具NuSMV进行一致性检验。最后，基于以上研究工作，设计并开发了UML检验工具。软件测试是保障软件质量的关键步骤，其核心问题是测试用例的自动生成。本文在研究了基于模型检测的测试用例自动生成方法的基础上，提出了一个基于二叉树快速生成算法来构造时序逻辑；结合基于需求、运用模型检测技术的测试用例自动生成流程，得到满足MC/DC覆盖准则的测试用例集。最后，设计并实现了一个基于模型检测的测试用例自动生成工具，结合航空电子系统，利用现有工具TestBed进行测试用例的正确性和覆盖率的验证。