随着现代航天科技的发展,嵌入式软件在航天领域的应用越来越广泛,航天嵌入式软件的规模、复杂度及其在整个航天系统中的功能比重急剧上升,呈现综合化、复杂化的发展趋势,导致对航天嵌入式软件的可靠性、安全性的要求越来越高。因此,如何提高航天嵌入式软件的可靠性、安全性成为人们越来越关注的问题。应用模型检测技术验证系统模型时,系统规模的增长会导致待检测系统的模型的状态空间快速增长,并且,对于不断增长的状态空间进行穷举遍历会导致计算缓慢,出现状态空间爆炸问题。由于航天嵌入式软件功能复杂,对其建模后状态数量多,因此,在模型检测时会产生状态空间爆炸的问题,影响验证效率。针对上述问题,本文重点研究嵌入式软件模型检测技术、嵌入式软件状态空间约简技术,设计并实现航天嵌入式软件模型验证系统,该系统实现从Sys ML状态图模型到SMV模型的自动转换、对模型的状态空间进行约简以及对待检测模型进行验证,并在航天应用软件中进行应用,缓解状态空间爆炸问题,提高了模型检测的效率,为航天嵌入式软件安全性的提高奠定技术基础。本文所做工作如下:1.嵌入式软件模型验证系统总体框架设计:针对当前航天领域嵌入式软件安全性验证系统的缺失,本文提出航天嵌入式软件模型验证系统总体框架,分为基于模型检测实现的嵌入式软件模型验证工具、基于邻接矩阵实现的嵌入式软件状态空间约简工具。2.嵌入式软件状态空间约简工具设计与实现:针对航天领域嵌入式软件功能复杂、建模后状态数量多、在模型检测过程中会产生状态空间爆炸的问题,本文研究基于邻接矩阵的状态空间约简技术,设计并实现嵌入式软件状态空间约简工具,缓解模型检测过程中的状态空间爆炸问题。3.嵌入式软件模型验证工具设计与实现:针对当前航天领域嵌入式软件安全性验证的需求,针对目前我国对航天嵌入式软件前期设计的质量保障不够充分的问题,本文研究基于模型驱动架构的模型检测技术,面向星弹载嵌入式实时、安全、关键应用,将模型检测技术应用在航天领域嵌入式软件设计研发过程中,设计并实现嵌入式软件模型验证工具,保障了航天嵌入式软件的安全性,从而提高嵌入式软件在我国航天领域的应用,提升国产航天嵌入式软件总体设计能力,提高航天嵌入式软件的安全性,从顶层解决阻碍未来航天嵌入式软件发展的技术瓶颈及潜在问题。