Title

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.

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.

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