μC/OS-Ⅱ中消息队列通信机制的形式化验证

摘要：

μC/OS-Ⅱ是一个可移植、可裁减的基于优先级的抢占式多任务实时内核,其代码主要用C语言编写.消息队列是一种被广泛使用且灵活的线程间的通信方式,它的安全性对于构建安全操作系统内核十分重要.针对μC/OS-Ⅱ中消息队列机制,给出消息接收和发送接口所操作的共享数据结构满足的数学规范,同时给出了这两个接口实现的安全性(safety)证明,相关的证明在定理证明工具Coq中完成.

关键词：μC/OS-Ⅱ、形式化验证、消息队列、安全性、Coq

所属期刊栏目：37

分类号：TP311(计算技术、计算机技术)

资助基金：国家自然科学基金项目61202052,61229201,61103023

在线出版日期：2016-10-25（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：1179-1184