航天嵌入式操作系统的分析与验证

摘要：

在介绍航天嵌入式操作系统的特点和应用概况的基础上，阐述了对航天嵌入式操作系统进行自动分析与验证的必要性，综述了自动分析和验证技术，并重点介绍了模型检测和符号执行两种分析技术，列举了领域内近年来具有代表性的工具及分析实例。结合航天嵌入式操作系统的特点，总结了嵌入式操作系统自动分析与验证技术面临的挑战，包括状态爆炸、描述不精确性、代码复杂度、实时性分析等。

关键词：嵌入式操作系统、分析验证、静态分析、模型检测、符号执行、航天系统

所属期刊栏目：18

分类号：TP316(计算技术、计算机技术)

资助基金：载人航天领域预先研究项目000301;国家自然科学基金项目61003028、61073044、60903051

在线出版日期：2013-01-27（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：69-74