Abstract
We describe our experience with verifying the schedulerrelated 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.
Cite
CITATION STYLE
Divakaran, S., D’Souza, D., Kushwah, A., Sampath, P., Sridhar, N., & Woodcock, J. (2015). Refinement-based verification of the FreeRTOS scheduler in VCC. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9407, pp. 170–186). Springer Verlag. https://doi.org/10.1007/978-3-319-25423-4_11
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
