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

Microkernel verification based on online model checking

作　　者：董星河 郭建[2] DONG Xinghe;GUO Jian(National Trusted Embedded Software Engineering Technology Research Center,ECNU,Shanghai 200062,China;Software/Hardware Co-design Technology and Application Engineering Research Center,MOE,ECNU,Shanghai 200062,China)

机构地区：[1]国家可信嵌入式软件工程技术研究中心华东师范大学,上海200062 [2]软硬件协同设计技术与应用教育部工程研究中心华东师范大学,上海200062

出　　处：《微纳电子与智能制造》2020年第1期102-109,共8页Micro/nano Electronics and Intelligent Manufacturing

基　　金：自然科学基金委重点项目(61532019);上海市重点项目(19511103602)资助。

摘　　要：物联网的兴起,对操作系统的可靠性提出了更高的要求。为确保微内核操作系统的安全性,提出了一种基于事件总线的微内核在线模型验证框架,主要思想是通过映射函数将源代码转换成抽象模型,并从微内核规范中抽取性质。根据源代码的控制流程图查找监控点并进行插桩;在微内核运行过程中,定期监测实际运行信息,并将之转化为抽象信息提交给抽象模型,通过有界模型检查,查看是否满足性质;若不满足,则表明源代码可能存在错误。最后,该验证框架应用于本团队自行开发的基于事件总线的微内核验证中。The development of internet of things(IoT)has put forward higher requirements on the reliability of operating system.In order to ensure safety of the microkernel operating system,this paper proposes an online model checking framework of the eventbus-based microkernel.The main idea is to transform the source code into an abstract model through mapping functions and to extract properties from the microkernel specification.The monitoring points are found through the control flowchart of the source code and instrumentation is used.While the microkernel is running,the actual executing information in the monitoring points is periodic monitored and is converted into abstract information,which is then transmitted to the abstract model.Using the bounded model checking method,the abstract model is verified whether to satisfy the properties.If not,a potential error is detected.In the end,the framework is applied to the eventbus-based microkernel verification.

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

分 类 号：TP316[自动化与计算机技术—计算机软件与理论]