10.3969/j.issn.1000-3428.2015.03.010
μC/OS-Ⅲ任务调度器在Coq中的验证
以μC/OS-Ⅲ内核中的任务调度器为研究对象,选取调度相关的核心代码,验证调度器代码满足优先调度最高优先级任务的性质。基于分离逻辑与SCAP验证理论,利用Coq辅助证明工具,通过定义机器模型、操作语义、逻辑断言以及推导规则构建验证框架。在验证框架中,定义内核数据结构和内核相关性质的逻辑描述,模块化地对内核代码进行推理。验证结果表明,μC/OS-Ⅲ任务调度器满足可靠性要求,并且可以通过机器的自动检查。
任务调度器、形式化验证、分离逻辑、Coq证明工具、最高优先级
TP309(计算技术、计算机技术)
国家自然科学基金资助青年项目61202052;国家自然科学基金海外及港澳学者合作研究基金资助项目61229201。
2015-04-03(万方平台首次上网日期,不代表论文的发表时间)
共6页
53-58