  FreeRTOS is a real-time operating system with configurable scheduling
policies. Its portability and configurability make FreeRTOS one of the most
popular real-time operating systems for embedded devices. We formally analyze
the FreeRTOS scheduler on ARM Cortex-M4 processor in this work. Specifically,
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.
