基于在线模型检验技术的微内核验证

• 作者: 董星河 郭建
• 来源期刊: 微纳电子与智能制造
• 学科: 工学
• 关键词: 操作系统 有界模型检查 映射函数 线性时态逻辑
• 年，卷（期）: 2020,（1）
• 页码范围: 102-109
• 页数: 8页
• 分类号: TP316

摘要

物联网的兴起,对操作系统的可靠性提出了更高的要求。为确保微内核操作系统的安全性,提出了一种基于事件总线的微内核在线模型验证框架,主要思想是通过映射函数将源代码转换成抽象模型,并从微内核规范中抽取性质。根据源代码的控制流程图查找监控点并进行插桩;在微内核运行过程中,定期监测实际运行信息,并将之转化为抽象信息提交给抽象模型,通过有界模型检查,查看是否满足性质;若不满足,则表明源代码可能存在错误。最后,该验证框架应用于本团队自行开发的基于事件总线的微内核验证中。

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	董星河		1	0	0.0	0.0
2	郭建		1	0	0.0	0.0