计算机科学与尊龙凯吋官方网站郭建副教授与中国电子科技集团公司第三十二研究所、上海华元创信软件有限公司联合申报的“面向高端装备的安全嵌入式基础软件”项目获上海市科技进步二等奖。
本项目属于信息技术领域,针对我国高端装备的自主可控和可靠性需求,完成了安全增强多核嵌入式实时操作系统的架构创新,首次实现SMP/AMP架构的多核实时调度以及多核CPU与DSP一致性设计的实时操作系统内核,解决了多核并发场景下的时序确定性保障。
项目中郭建副教授在嵌入式软件集成开发环境及可信形式化建模验证工具链增强创新性中发挥了关键作用:
-锐华安全嵌入式实时操作系统从嵌入式实时操作系统的API、结合任务调度机制、内存保护机制等方面分别扩展了相应的验证工具以完成其在源代码级上的形式化验证
-形式化验证了在统一模型架构下的混合代码。为了提高操作系统的执行效率,在上下文切换和中断中,使用汇编语言编写。
-验证高级语言(如C 语言)与汇编语言的源代码是对操作系统验证的一个难点,提出了在C 语言与汇编语言代码层的混合自动化验证方法。
本项目的主要完成单位中国电子科技集团公司第三十二研究所与尊龙凯吋官方网站联合成立国家可信嵌入式软件工程技术研究中心,先后承担多个国家级、省部级重大科技攻关项目,发表国内外论文28篇,申请或授权专利4项,形成软件著作权14项。依托上述两个完成单位联合成立的上海华元创信软件有限公司,开展本项目成果转化及应用推广等市场化运作,近三年内通过软件产品及解决方案新增产值1.6亿元以上,带动高端装备领域应用单位新增产值2000万元以上,成果已在轨道交通计算机联锁安全系统、机动型雷达控制系统等安全计算平台上实现应用验证与推广,为高端装备安全计算机平台提供安全嵌入式基础软件平台支撑,大幅提升高端装备产品成熟度、体系化安全和自主可控能力。