μC/OS-Ⅲ任务调度器在Coq中的验证

• 作者: 罗尔聪 郭宇
• 来源期刊: 计算机工程
• 学科: 工学
• 关键词: 任务调度器 形式化验证 分离逻辑 Coq证明工具 最高优先级
• 年，卷（期）: 2015,（3）
• 所属期刊栏目: 体系结构与软件技术
• 页码范围: 53-58
• 页数: 6页
• 分类号: TP309
• 字数: 4521字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-3428.2015.03.010

摘要

以μC/OS-Ⅲ内核中的任务调度器为研究对象，选取调度相关的核心代码，验证调度器代码满足优先调度最高优先级任务的性质。基于分离逻辑与SCAP验证理论，利用Coq辅助证明工具，通过定义机器模型、操作语义、逻辑断言以及推导规则构建验证框架。在验证框架中，定义内核数据结构和内核相关性质的逻辑描述，模块化地对内核代码进行推理。验证结果表明，μC/OS-Ⅲ任务调度器满足可靠性要求，并且可以通过机器的自动检查。

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	郭宇	中国科学技术大学计算机科学与技术学院	12	38	3.0	6.0
5	罗尔聪	中国科学技术大学计算机科学与技术学院	1	1	1.0	1.0