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