复杂内核数据结构的形式化描述和验证

摘要：

对数据结构进行形式化描述是内核验证的重要组成部分,但是在实际的验证工作中,内核经常会使用一些不规则的数据结构,而对不规则数据结构的形式化定义仍存在诸多困难.针对内核中的复杂数据结构,本文提出使用结构拆分以及形状和内存分离的方法来形式化定义内核中的不规则数据结构,并运用该方法成功刻画了某航天操作系统内核的进程管理数据结构,最终成功验证了该内核中相关API的代码.相关的代码验证工作在定理证明工具Coq中完成.

关键词：内核数据结构、形式化验证、分离逻辑、内核验证

所属期刊栏目：40

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

资助基金：国家自然科学基金项目 61632005, 61502031 资助

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

页数：共8页

页码：359-366