近日，计算机学院赵永望的研究小组收到来自美国波音公司Associate Fellow、ARINC653国际标准委员会主席的邮件，对其团队在ARINC653航空机载操作系统标准的研究成果表示认可与致谢，并将在ARINC653标准新版本中对存在的安全缺陷进行修复。

ARINC653标准是国际航空工业界实时操作系统的事实性标准，已有20年历史，被航空航天领域绝大多数实时操作系统所遵循，已应用到空客A380、波音787、F22、NASA猎户座飞船等。该标准委员会主席由来自波音和空客的两位专家担任，成员包括波音、空客、洛克希德马丁、GE航空、霍尼韦尔、达索航空、风河等。

计算机学院近年来一直从事安全关键实时操作系统的形式模型与证明研究，并与新加坡南洋理工大学、欧盟FP7 EURO-MILS项目、法国科学院IRIT研究所等开展紧密合作。该项研究成果利用形式化方法构建了完整的实时操作系统规约，并通过自动化手段完成1600多个定理的形式证明，最终发现了ARINC653标准的6个安全缺陷。相关成果已发表在ISSRE 2015国际会议（软件可靠性领域顶级会议）和IEEE Transactions on Industrial Informatics期刊。论文受到ARINC653标准委员会的高度关注， 2016年10月ARINC653标准委员会召开主题会议讨论了我们的成果。最终，标准委员会确认ARINC653存在上述安全缺陷，并计划在其新版本中进行修复。

[以下是美国波音公司发来的致谢邮件]