Program Verification of FreeRTOS Using Microsoft Dafny

FreeRTOS is a popular real-time and embedded operating system. Real-time software requires code reviews, software tests, and other various quality assurance activities to ensure minimal defects. This free and open-source operating system has claims of robustness and quality [26]. Real-time and embedded software is found commonly in systems directly impacting human life and require a low defect rate. In such critical software, traditional quality assurance may not suce in minimizing software defects. When traditional software quality assurance is not enough for defect removal, software engineering formal methods may help minimize defects. A formal method such as program verication is useful for proving correctness in real-time software. Microsoft Research created Dafny for proving program correctness. It contains a programming language with specication constructs. A program verication tool such as Dafny allows for proving correctness of FreeRTOS\u27s modules. We propose using Dafny to verify the correctness of FreeRTOS\u27 scheduler and supporting AP