《表1 统计结果：复杂内核数据结构的形式化描述和验证》
提示：宽带有限、当前游客访问压缩模式
作者在某航天操作系统内核的进程管理结构定义的基础之上成功验证了该内核的任务创建和任务调度模块的代码.其中任务创建模块涉及了对就绪链表的插入操作，任务调度模块涉及对就绪链表的遍历操作.实现任务创建模块的C代码共计大约70行，任务调度模块中调用了上下文切换函数，实现上下文切换和任务调度的C代码共计约60行.所有的代码证明都是在定理证明工具Coq中进行的，其中用于验证任务创建模块的Coq脚本共计约5300行，用于验证任务调度模块的Coq脚本共计约1660行.统计结果见表1.
| 图表编号 | XD0060253800 严禁用于非法目的 |
|---|---|
| 绘制时间 | 2019.02.01 |
| 作者 | 马顶、付明、乔磊、冯新宇 |
| 绘制单位 | 中国科学技术大学计算机科学与技术学院、华为上海研究所2012实验室-OS内核实验室、北京控制工程研究所、南京大学计算机软件新技术国家重点实验室 |
| 更多格式 | 高清、无水印（增值服务） |
