Formal Analysis of FreeRTOS Scheduler on ARM Cortex-M4 Cores

FreeRTOS is a real-time kernel with configurable scheduling policies. It is one of the most popular real-time kernel for embedded deviced due to its portability and configurability. We formally analyze the FreeRTOS scheduler on ARM Cortex-M4 processor in this work. Concretely, we build a formal model for the FreeRTOS ARM Cortex-M4 port and apply model checking to find errors in our models for FreeRTOS example applications. Intriguingly, several errors are found in our application models under different scheduling policies. In order to confirm our findings, we modify application programs distributed by FreeRTOS and reproduce assertion failures on the STM32F429I-DISC1 board.