软件测试在软件的整个开发过程中占有非常重要的地位,是保证软件质量的关键步骤。航空软件具有实时性、嵌入性、高可靠性等特点,对其进行严格的软件测试至关重要。测试用例生成是软件测试的核心问题,研究适用于航空软件的测试用例自动生成方法,对提高航空软件的可靠性有着重要的理论意义和实用价值。本文以在某研究所参与的航空软件――卫星导航系统测试项目为研究背景,首先,在对国内外已有的测试用例自动生成研究成果深入分析的基础上,研究了基于模型检查的测试用例自动生成方法。结合航空软件灰盒测试过程,提出了一个基于需求、运用模型检查技术的测试用例自动生成流程,该流程涉及软件需求抽象、软件需求的形式化系统建模、基于测试准则的时序逻辑变换、软件需求形式化模型与时序逻辑的一致性验证以及测试用例的提炼和整理等内容。其次,依据航空软件测试标准DO-178B的要求,本文提出一个布尔运算符替换算法来构造时序逻辑,该时序逻辑经过模型检查后得到的用例能够满足MC/DC覆盖准则。最后,本文针对测试用例自动生成流程,设计开发了一个基于模型检查测试用例自动生成工具。根据卫星导航系统的软件测试过程,通过将该工具作为设计测试用例的辅助工具,并设计测试驱动模板,以及进行结构覆盖分析,对提出的测试用例自动生成方法实用性进行了验证。