Formally verifying FreeRTOS’ interprocess communication mechanism
FreeRTOS is a real-time kernel and set of libraries for Internet of Things (IoT) applications. The FreeRTOS kernel provides a portable abstraction layer, task scheduling and interprocess communication (IPC) mechanisms. The main IPC mechanism in FreeRTOS is a concurrent queue: a circular buffer data structure that tasks and interrupt service routines use to exchange messages. As a fundamental building block for larger applications, the correctness of the queue implementation is vital. We have formally verified the memory safety, thread safety and functional correctness of this queue implementation using deductive verification. Our proofs are publicly available and give machine-checkable assurances of correctness that would be infeasible to obtain through testing alone.