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

• 作者: 刘剑 李斌 李潇 马越
• 来源期刊: 载人航天
• 学科: 工学
• 关键词: 嵌入式操作系统 分析验证 静态分析 模型检测 符号执行 航天系统
• 年，卷（期）: 2012,（6）
• 所属期刊栏目: 工程技术
• 页码范围: 69-74
• 页数: 6页
• 分类号: TP316
• 字数: 4522字
• 语种: 中文

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李斌	中国科学院软件研究所基础软件国家工程研究中心	372	5610	37.0	58.0
2	李潇	中国科学院软件研究所基础软件国家工程研究中心	23	130	7.0	10.0
3	刘剑	中国科学院软件研究所基础软件国家工程研究中心	66	379	12.0	17.0
4	马越	中国科学院软件研究所基础软件国家工程研究中心	8	28	4.0	5.0