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

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