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

Verification of μC/OS-Ⅲ Task Scheduler in Coq

作　　者：罗尔聪 郭宇[1,2] 

机构地区：[1]中国科学技术大学计算机科学与技术学院,合肥230026 [2]中国科学技术大学苏州研究院软件安全实验室,江苏苏州215123

出　　处：《计算机工程》2015年第3期53-58,共6页Computer Engineering

基　　金：国家自然科学基金资助青年项目(61202052);国家自然科学基金海外及港澳学者合作研究基金资助项目(61229201)

摘　　要：以μC/OS-Ⅲ内核中的任务调度器为研究对象,选取调度相关的核心代码,验证调度器代码满足优先调度最高优先级任务的性质。基于分离逻辑与SCAP验证理论,利用Coq辅助证明工具,通过定义机器模型、操作语义、逻辑断言以及推导规则构建验证框架。在验证框架中,定义内核数据结构和内核相关性质的逻辑描述,模块化地对内核代码进行推理。验证结果表明,μC/OS-Ⅲ任务调度器满足可靠性要求,并且可以通过机器的自动检查。This paper studies the task scheduler in a widely used embeddedμC/ OS-Ⅲkernel. After selecting core parts from the scheduler,it specifies the properties of the scheduler formally. Based on the separation logic and SCAP,it builds a verification framework including a machine model,operational semantics,assertion languages,and inference rules. In the framework,assertions specifying system data structures and properties are defined,and system code is able to be reasoned about modularly. Finally,the properties of the task scheduler inμC/ OS-Ⅲare formally proved,and the entire proof provided by the work are machine checkable.

关 键 词：任务调度器 形式化验证 分离逻辑 Coq证明工具 最高优先级 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]