Refinement-Based Verification of the FreeRTOS Scheduler in VCC
Formal Methods and Software Engineering (Lecture Notes in Computer Science series)
We describe our experience with verifying the scheduler-related functionality of FreeRTOS, a popular open-source embedded real-time operating system. We propose a methodology for carrying out refinement-based proofs of functional correctness of abstract data types in the popular code-level verifier VCC. We then apply this methodology to carry out a full machine-checked proof of the functional correctness of the FreeRTOS scheduler. We describe the bugs found during this exercise, the fixes made, and the effort involved.
Divakaran, Sumesh; D’Souza, Deepak; Kushwah, Anirudh; Sampath, Prahladavaradan; Sridhar, Nigamanth; and Woodcock, Jim, "Refinement-Based Verification of the FreeRTOS Scheduler in VCC" (2015). Electrical Engineering & Computer Science Faculty Publications. 338.
S. Divakaran, D. D'Souza, A. Kushwah, P. Sampath, N. Sridhar and J. Woodcock, "Formal Methods and Software Engineering: 17th International Conference on Formal Engineering Methods, ICFEM 2015, Paris, France, November 3-5, 2015, Proceedings," pp. 170-186, 2015.