Refinement-Based Verification of the FreeRTOS Scheduler in VCC
Document Type
Conference Proceeding
Publication Date
2015
Publication Title
Formal Methods and Software Engineering (Lecture Notes in Computer Science series)
Abstract
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.
Repository Citation
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 and Computer Engineering Faculty Publications. 338.
https://engagedscholarship.csuohio.edu/enece_facpub/338
Original Citation
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.
DOI
10.1007/978-3-319-25423-4 11
Volume
9407
Comments
Paper presented at 17th International Conference on Formal Engineering Methods, ICFEM 2015, Paris, France, November 3-5, 2015.
Supported by grants from the UK-India Education and Research Initiative (UKIERI) and the Robert Bosch Center for Cyber Physical Systems, IISc, Bangalore.