项目编号 | R33-2019-J001 |
项目名称 | 航天嵌入式软件可信性保障关键技术和应用 |
候选单位 | 北京控制工程研究所 北京轩宇信息技术有限公司 中国科学院软件研究所 华东师范大学 中国人民解放军国防科技大学 南京大学 |
候选人 | 顾 斌 郭向英 陈 睿 詹乃军 蒲戈光 毛晓光 王 政 董晓刚 赵建华 陈仪香 乔 磊 陈立前 高栋栋 赵 雷 辛优美 |
项目简介 | 嵌入式软件是航天器的重要组成部分,其可信性直接影响航天任务成败。随着我国航天事业的快速发展,嵌入式软件的数量、复杂性和规模急剧增加,已成为航天工程研制的瓶颈。如何更好、更快地研制嵌入式软件是国家航天发展的重大需求。
航天嵌入式软件具有强实时、中断并发、控制模式转换复杂等特点,其可信性保障是国内外公认的重大挑战。项目组依托国家自然科学基金“可信软件基础研究”重大研究计划,历经10余年的理论、技术创新和工程实践,提出并建立了以技术体系为核心、以标准、规范和工具为手段的软件可信保障系统解决方案。主要创新点如下:
1.建立了航天嵌入式软件可信保障技术体系,揭示了软件可信保障的机理,首次系统地回答了软件可信保障的内容及其相互关系,解决了嵌入式软件可信性系统保障的理论难题,研发了具有完全自主知识产权的可信保障集成环境,实现了软件交付后千行代码缺陷率下降90%,生产率提升20%以上。
2.建立了嵌入式软件缺陷预防、检测和定位的成套方法,突破了可信编程、数值型缺陷检测、中断数据访问冲突检测、动态时序建模和验证及缺陷准确定位等核心技术,研制了配套的保障工具集,解决了并发多重中断驱动嵌入式软件动态时序和程序实现正确性保障的难题,软件缺陷检测效率提高3倍以上。
3.提出了一种利用高阶Lie-导数的混成系统渐近稳定性判定方法和一种基于变量替换的带有超越函数混成系统抽象方法,解决了混成系统渐近稳定性判定和安全性形式验证的理论难题,实质性地推动了混成系统验证技术的进步,首次实现了我国航天关键复杂嵌入式软件控制行为的形式验证。
4.提出了融合开发过程、软件产品、可信要素、工具使用等多维属性的航天嵌入式软件可信性分级度量评估方法,建立了基于全生命周期的可信性分级度量模型,研制了可信度量评估工具,解决了嵌入式软件可信性定量度量的难题,实现了嵌入式软件从分散的可信侧面定性度量向系统化定量度量的转变。
本项目出版专著1部,发表论文80余篇,培养博士后6名、博士38名、硕士70名,获国家授权发明专利30项、软件著作权18项,研制了16套可信保障工具和集成环境。
本项目成果已在载人航天和探月工程等国家重大专项中全面应用,系统地保障和显著提高了我国航天嵌入式软件的可信性,实现了软件可信性保障从局部到系统、从依赖人到依赖工具的转变,满足了航天任务对软件的可信需求。并广泛应用到军民多个安全关键领域,近三年经济效益达2.97亿元,社会经济效益巨大。 |
关 闭 |