随着软件在我国航天领域中得到越来越广泛的使用,对软件的可靠性要求,尤其是在型号软件系统中,得到了越来越多的重视。软件失效将会带来巨大的经济损失,甚至会直接导致更为严重的事故或灾难。为了避免软件错误带来的损失,从测试角度来看,必须要尽可能多的发现软件中存在的隐患,提高软件的可靠性。研究先进的软件测试技术,并通过设计开发具体的工具将先进的测试技术加以实现,对提高航天型号软件的可靠性具有十分重要的意义。本文首先通过对国内外测试用例自动生成方法及自动化测试的研究分析,提出若干目前相关研究可以借鉴的技术成果,并指出它们的不足和改进方向。在调研国内外研究成果的基础上,针对在形式化建模过程中对状态变量的标识和跟踪困难等问题,实现了一种定位功能机制,全程跟踪和准确定位形式化模型中的状态量,从而在很大程度上提高了建模效率。其次,在对测试覆盖准则的分析基础上,选取了简单转移覆盖与基于MC/DC覆盖准则要求,并对这两种典型且具有不同代表性的覆盖准则加以研究分析,使测试用例对软件进行测试时满足不同安全等级的测试覆盖要求。第三,通过模型检查器,从形式化模型生成结果中提取出来反例,针对反例中出现的重复和短前缀冗余,设计去除冗余算法,精简反例集合。第四,通过设计一种状态变量输入输出划分功能机制,可以实现直接从反例中提取出测试用例,再通过把测试用例转换为测试脚本,实现生成自动化测试的基础。借助批处理测试驱动文件,完成自动化测试过程并生成测试比对结果。在以上研究的基础上,总结了一套针对航天软件需求的确认测试用例自动生成及自动化测试流程,该流程涉及软件需求的形式化建模,基于测试准则的时序逻辑变换,反例的提取和精简,测试用例的整理生成以及自动化测试等内容。针对上述流程,设计并开发了一套能运用于型号软件的测试用例自动生成及自动化测试的软件工具。最后,本文将基于软件需求建模的测试用例自动生成工具应用于一个具有典型的安全性可靠性要求的净化工作室软件测试中,对该工具的有效性和实用性加以证明;同时为基于软件需求建模的测试用例自动生成工具在其他型号软件中的应用提供指导。