Program Verification of FreeRTOS using Microsoft Dafny
Matthew John Matias · EngagedScholarship @ Cleveland State University (Cleveland State University) · 2014
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's modules. We propose using Dafny to verify the correctness of FreeRTOS' scheduler and supporting API