随着技术的发展,在航天领域,软件在型号系统中得到了广泛的应用。软件失效会直接导致严重的事故甚至灾难。为提高软件的可靠性,对于软件测试而言,需尽可能多的发现软件中可能存在的错误,提高对软件测试的充分性。探索先进的软件测试技术以提高软件测试水平,对提高航天型号软件的可靠性具有十分重要的意义。本课题首先调研了国内外确认测试用例自动生成研究现状,并总结出目前相关研究的可以借鉴的技术成果,以及需要改进的地方。然后在调研国内外研究成果的基础上,分析了各种方法的优缺点,确立了以模型检查技术为基础,研究可行的,能运用于实际型号软件中的自动生成测试用例的方法的路线方针。其次,在确立的技术路线的基础上,提出一种有效的描述需求中数值计算特性的技术途径,使模型检查技术能够运用于实际的型号软件中。第三,在制定的基于需求模型的MC/DC覆盖准则的基础上,提出了一种构造时序逻辑的算法,使构造的时序逻辑经过模型检查后得到的用例能够达到MC/DC覆盖准则的要求。在以上研究的基础上,总结了一套针对型号软件需求的确认测试用例自动生成流程,该流程涉及软件需求分析、软件需求的形式化建模、软件需求与形式化模型一致性验证、基于测试准则的时序逻辑变换以及测试用例的提炼和整理等内容。论文详细的介绍了测试用例自动生成方法的工序流程。最后,本课题将测试用例自动生成方法首次应用到实际的型号软件中,即智能电源控制器,将自动生成的测试用例与人工设计的测试用例进行比较,检验其生成的用例的有效性和充分性,证明该方法的实用性。该成果可以为自动生成用例方法在其他型号软件中的应用提供指导。