计算机工程Issue(3)：53-58,6.DOI:10.3969/j.issn.1000-3428.2015.03.010
μC/OS-Ⅲ任务调度器在Coq中的验证
Verification of μC/OS-Ⅲ Task Scheduler in Coq
摘要
Abstract
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证明工具/最高优先级Key words
task scheduler/formal verification/separation logic/Coq proof tool/highest priority分类
信息技术与安全科学引用本文复制引用
罗尔聪,郭宇..μC/OS-Ⅲ任务调度器在Coq中的验证[J].计算机工程,2015,(3):53-58,6.基金项目
国家自然科学基金资助青年项目(61202052) （61202052）
国家自然科学基金海外及港澳学者合作研究基金资助项目(61229201)。 （61229201）
