Information Sceicences Seminar——安全攸关操作系统的形式化验证
主 题: Information Sceicences Seminar——安全攸关操作系统的形式化验证
报告人: Yongwang Zhao (Beihang University)
时 间: 2018-03-21 13:00-15:00
地 点: Room 1303, Sciences Building No. 1
报告人简介：赵永望，博士，副教授。中国计算机学会(CCF)高级会员、 CCF形式化方法专委/系统软件专委委员、ARINC 653国际操作系统标准委员会委员、国家信息技术标准化技术委员会分委会专家。曾任国际标准化组织 ISO/IEC JTC1 SOA研究组组长、新加坡南洋理工大学高级研究员。主要研究方向包括操作系统内核及安全、形式逻辑与验证、安全攸关系统与模型驱动方法等。主持和参与了国家自然基金课题、国家核高基重大专项、新加坡NRF重大项目等十余项。2011年获得中国电子学会电子信息科技一等奖，2017年获得山东省科技进步一等奖。在IEEE Transactions on Dependable and Secure Computing、IEEE Transactions on Industrial Informatics、Journal of Systems and Software、TACAS、ISSRE等期刊/会议发表论文50余篇，担任IEEE Access期刊副主编。
摘要：安全攸关系统是指系统失效往往引起重大生命或财产损失的系统，广泛应用于航空/航天、核电、交通运输、医疗等领域。操作系统处于软件栈的最底层，对安全攸关系统起到至关重要的作用，对其开展形式化验证是高安全等级认证的必要途径，具有重大的工业需求和研究挑战。本报告主要介绍面向安全攸关操作系统的工业级形式化方法，并介绍我们在操作系统需求、设计、源代码、硬件指令集等层面的验证方法和成果。相关成果得到美国波音公司、法国空客公司等的认可，被纳入航空/航天国际操作系统标准，并在开源操作系统社区产生影响力。
