随着航天科学技术的飞速发展，航天软件的规模更大，更复杂，安全问题也日益突出。而数值型运行时错误(Run-time Errors)在实际应用中是影响航天软件安全性的重要因素。运行时错误是相对于编译错误出现在软件动态运行时，导致预定义之外的不正确结果或者处理器停机的错误。　　目前运行时错误检测其中一种有效方法是形式化分析，其中抽象解释和模型检验是最主流的方法。基于抽象解释的程序分析进行运行时错误检测能够提供完备的分析结果，但是目前已有的许多抽象域的并未针对航天软件的特点，对航天软件分析的精度和分析的效率不能很好的权衡。而模型检验通过穷尽程序状态搜索满足验证属性的状态，能够精确检测运行时错误，但是容易出现状态空间爆炸，即使通过限定界的有界模型检验能够避免该问题，却不能证明程序中不存在运行时错误。　　在进行基于抽象解释分析的过程中，为了更有效的分析航天嵌入式C程序，结合航天软件的特点，本论文提出两个抽象域。针对航天软件中多矩阵运算的特点，为了在分析该类软件时更好的权衡分析的精度和效率，提出区间向量抽象域。通过将矩阵抽象为两个区间向量，用区间向量之间的运算来逼近实际程序中的矩阵运算。　　针对航天软件中多浮点运算的特点，为了提高在分析该类软件时的效率，避免使用大数库中多精度浮点数带来的复杂计算，提出基于浮点补偿的八边形抽象域。通过使用带补偿量的机器浮点数替代使用大数库中多精度浮点数来改进传统八边形抽象域。　　本论文为了降低运行时错误检测的漏报率和误报率，提出通过结合抽象解释和有界模型检验优势的运行时错误检测方法。首先对源程序使用抽象解释理论对程序进行分析获得程序不变量，并结合运行时错误属性插入相应的断言。然后采用有界模型检验验证断言的正确性。通过对程序先基于抽象解释进行分析获得完备的结果，可以防止运行时错误的漏报，弥补仅使用有界模型检验不完备的缺点。然后通过有界模型检验能够较精确的验证断言的正确性，降低仅使用抽象解释分析的误报率。如果验证成功，表示插入的断言正确，不存在运行时错误。如果验证失败，说明插入的断言有误，存在运行时错误。　　实验结果说明，本论文提出的程序数值型运行时错误检测方法与现有仅使用抽象解释或者仅使用模型检验方法相比，降低了运行时错误检测的漏报率和误报率。