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

摘要：

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

关键词：操作系统、有界模型检查、映射函数、线性时态逻辑

所属期刊栏目：2

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

资助基金：自然科学基金委重点项目;上海市重点项目

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

页数：共8页

页码：102-109