|
|||||
|
|
| μC/OS-Ⅲ任务调度器在Coq中的验证 | |
| 作者姓名： | 罗尔聪 郭宇 |
| 作者单位： | 中国科学技术大学计算机科学与技术学院，合肥230026; 中国科学技术大学苏州研究院软件安全实验室，江苏 苏州215123 |
| 基金项目： | 国家自然科学基金资助青年项目(61202052);国家自然科学基金海外及港澳学者合作研究基金资助项目(61229201) |
| 摘 要： | 以μC/OS-Ⅲ内核中的任务调度器为研究对象，选取调度相关的核心代码，验证调度器代码满足优先调度最高优先级任务的性质。基于分离逻辑与SCAP验证理论，利用Coq辅助证明工具，通过定义机器模型、操作语义、逻辑断言以及推导规则构建验证框架。在验证框架中，定义内核数据结构和内核相关性质的逻辑描述，模块化地对内核代码进行推理。验证结果表明，μC/OS-Ⅲ任务调度器满足可靠性要求，并且可以通过机器的自动检查。 |
| 关 键 词： | 任务调度器 形式化验证 分离逻辑 Coq证明工具 最高优先级 |
| 本文献已被 CNKI 万方数据 等数据库收录！ | |