%0 Journal Article
%T μC／OS-Ⅱ中消息队列通信机制的形式化验证
%A 付明
%A 冯新宇
%A 马杰波
%J 中山大学学报（自然科学版）
%D 2016
%X 摘要 μC／OS-Ⅱ是一个可移植、可裁减的基于优先级的抢占式多任务实时内核，其代码主要用C语言编写.消息队列是一种被广泛使用且灵活的线程间的通信方式，它的安全性对于构建安全操作系统内核十分重要.针对μC／OS-Ⅱ中消息队列机制，给出消息接收和发送接口所操作的共享数据结构满足的数学规范，同时给出了这两个接口实现的安全性（safety）证明，相关的证明在定理证明工具Coq中完成
%K μC／OS-Ⅱ
%K 形式化验证
%K 消息队列
%K 安全性
%K Coq
%U http://xwxt.sict.ac.cn/CN/abstract/abstract3434.shtml