讲坛题目：IMA架构下的分区安全属性的验证需求

主 讲 人：叶宏 研究员

讲座时间：2023年6月2日，下午14:00（腾讯会议号：706 316 350）

主办单位：研究生院

承办单位：计算机科学与工程学院

摘要：本报告主要介绍有关IMA的分区安全属性的形式化验证需求和航空电子系统的基本概念和发展历程。首先重点讲解了综合化、模块化航空电子系统（IMA）的定义、作用和架构，分析了五类与安全有关的功能需求。其次，介绍IMA架构下的分区技术的核心概念、特征和工作原理，分析了分区安全属性传统验证方法的难处，讨论了国外使用形式化方法对强分区操作系统验证情况，给出了分区安全属性的建模及验证需求，以及适合采用的形式化模型。最后，介绍DO-333机载软件适航标准对形式化方法的适航要求和建议方法。

个人简介：叶宏，中国航空工业集团西安航空计算技术研究所研究员，副总工程师，享受国家政府特殊津贴专家，航空工业集团特级专家。中国计算机学会（CCF）高级会员，形式化/嵌入式系统专委会常委。长期从事航空装备安全攸关软件的研究和研制工作，曾主持30余项国家重点预先研究、国家重点自然基金、国家“核高基”专项以及航空装备型号任务。作为国产天脉操作系统的总设计师，主持研制了多系列的天脉产品，覆盖多种应用领域，已被我国各种军用机型飞机规模应用，其成果在国内出处于领先地位。曾获得部级国防科技成果奖10项，省部科技成果奖14项，个人荣立航空集团功7项，获国家发明专利12项，发表学术论文（合编、专著、国军标等）30余篇。主要研究方向包括嵌入式系统、操作系统、航空电子系统、安全攸关系统和软件安全性可靠性等技术。