講壇題目:IMA架構下的分區安全屬性的驗證需求
主 講 人:葉宏 研究員
講座時間:2023年6月2日,下午14:00(騰訊會議號:706 316 350)
主辦單位:研究生院
承辦單位:計算機科學與工程學院
摘要:本報告主要介紹有關IMA的分區安全屬性的形式化驗證需求和航空電子系統的基本概念和發展歷程。首先重點講解了綜合化、模塊化航空電子系統(IMA)的定義、作用和架構,分析了五類與安全有關的功能需求。其次,介紹IMA架構下的分區技術的核心概念、特征和工作原理,分析了分區安全屬性傳統驗證方法的難處,討論了國外使用形式化方法對強分區操作系統驗證情況,給出了分區安全屬性的建模及驗證需求,以及適合采用的形式化模型。最后,介紹DO-333機載軟件適航標準對形式化方法的適航要求和建議方法。

個人簡介:葉宏,中國航空工業集團西安航空計算技術研究所研究員,副總工程師,享受國家政府特殊津貼專家,航空工業集團特級專家。中國計算機學會(CCF)高級會員,形式化/嵌入式系統專委會常委。長期從事航空裝備安全攸關軟件的研究和研制工作,曾主持30余項國家重點預先研究、國家重點自然基金、國家“核高基”專項以及航空裝備型號任務。作為國產天脈操作系統的總設計師,主持研制了多系列的天脈產品,覆蓋多種應用領域,已被我國各種軍用機型飛機規模應用,其成果在國內出處于領先地位。曾獲得部級國防科技成果獎10項,省部科技成果獎14項,個人榮立航空集團功7項,獲國家發明專利12項,發表學術論文(合編、專著、國軍標等)30余篇。主要研究方向包括嵌入式系統、操作系統、航空電子系統、安全攸關系統和軟件安全性可靠性等技術。