摘要
μC/OS-Ⅱ是一个可移植、可裁减的基于优先级的抢占式多任务实时内核,其代码主要用C语言编写.消息队列是一种被广泛使用且灵活的线程间的通信方式,它的安全性对于构建安全操作系统内核十分重要.针对μC/OS-Ⅱ中消息队列机制,给出消息接收和发送接口所操作的共享数据结构满足的数学规范,同时给出了这两个接口实现的安全性(safety)证明,相关的证明在定理证明工具Coq中完成.
μC/OS-Ⅱ is a priority-based preemptive real-time multitasking operating system kernel for microprocessors, written mainly in the C programming language. Message queue is a flexible mechanism widely used to do thread communication. The reliability of the implementation of message queues is extremely important for constructing safe operating system kernel. This paper verifies the safety property of message queues in μC/OS-Ⅱ. We give the formal specification for the shared data structures used in the message queue and prove the correctness of two APIs （ OSQPend and OSQPost ） in Coq.
出处
《小型微型计算机系统》
CSCD
北大核心
2016年第6期1179-1184,共6页
Journal of Chinese Computer Systems
基金
国家自然科学基金项目(61202052
61229201
61103023)资助
