软件已成为国民经济、国防建设和人民生活基础设施的核心，然而软件的可信性令人担忧，特别是在航天/航空等安全攸关领域，微小的程序缺陷都可能导致机毁人亡的严重后果。如何保障软件系统，特别是安全攸关软件系统的可信性是计算机软件领域面临的重大技术挑战。在此背景下，西安电子科技大学与航天五院五〇二所开展了安全攸关软件验证方法和技术研究，突破了关键技术，形成了核心专利群，研发了工具集，构建了国产的安全攸关软件资源共享和协同验证平台MSV，以航天控制软件系统的可信性验证为实践环境，为提升我国航天软件的发展提供了关键技术支撑和实践指南。

项目揭示了以MSVL统一验证方法，抽象精化方法和动静结合方法为核心的大规模安全攸关软件可信性验证的机理，系统地提出了软件可信性验证MSV方法，产生了三方面技术方法：

1、发明了基于MSVL的集建模、仿真和验证为一体的统一验证理论，以MSVL编写程序，以命题投影时序逻辑PPTL公式描述性质，使得程序模型和性质描述基于同一逻辑体系，避免了"软件系统模型难以提取"的问题，并且将性质的验证转换为程序的执行，大幅度提高了验证效率。研制了建模、仿真和验证工具平台MSV，支持对系统的编译执行及建模，并且可对PPTL描述的系统完全正则性质包括区间相关性质和周期重复性质等进行形式化验证。支持 C、Verilog、VHDL程序和Petri网自动验证。

2、发明了基于多项式复杂度的抽象模型精化算法，解决了图灵奖获得者Clarke等人提出的精化方法中的指数爆炸问题，可以得到更小的精化模型，从而有效提高了抽象模型精化的效率；发明了线性复杂度的虚假路径检测算法，克服了Clarke等人提出的虚假反例路径检测中的多项式时间复杂度，且可以并行执行，在处理同等规模的路径时，效率远高于原有的SplitPath算法。

3、发明了基于CEGAR的动静结合验证方法，通过构造C程序的控制流自动机CFA，并且根据性质取非后的带标签的范式图LNFG构造扩展的抽象可达树eART，检测是否有反例路径，若存在，则使用SMT求解器Z3求解出输入变量的值，采用MSVL统一验证方法检测反例路径是否虚假，从而实现了对C程序的完全正则性质的验证，解决了验证过程中出现的误报或漏报问题，提高了验证的精确度。开发了动静结合验证工具SDMC，支持C程序时序性质的高效验证。

项目形成美国专利1项，中国发明专利20余项，在TSE、TKDE、ICSE、ASE和IJCAI等国际顶级期刊和会议发表论文60余篇，受到了多位国际著名学者的积极评价。发明人受邀在国内外重要论坛和学术会议做主题报告20余次，第一完成人获国家自然科学基金优秀青年基金资助。

项目探索形成了技术成果专利化，专利推广标准化，工具环境服务化，人才培养大众化的成果转换模式。MSV成功应用于我国探月工程三期月地高速再入返回飞行器等多款航天软件，检查出了一些深度隐藏的错误隐患。作为一款由我国自主研发的软件可信性验证工具，MSV在国家航天重大工程中做出了突出贡献，支持了我国航空、航天等关键领域的可信软件生产。此外，应用MSV首次检测出了目前正在使用的9个主要浏览器关于SSL/TLS协议实现的35处安全漏洞，11处已被相关公司或组织确认/修复。在修复过程中，相关技术人员充分利用了MSV提供的反例路径信息。项目主要成果编入中国计算机学会2017-2018中国计算机科学技术发展报告。项目提出的MSVL程序验证语言得到国际关注，到目前为止已召开8届SOFL+MSVL国际研讨会。项目的研究成果已经得到国内外研究学者的认可，并获得了高度的评价。