首页 | 本学科首页   官方微博 | 高级检索  
     

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

关 键 词:任务调度器  形式化验证  分离逻辑  Coq证明工具  最高优先级
本文献已被 CNKI 万方数据 等数据库收录!
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号