Paper Info
Title
Refinement-Based Verification of the FreeRTOS Scheduler in VCC.
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.
Year
Venue
Field
2015
ICFEM
Abstract data type,Programming language,Computer science,Correctness,Theoretical computer science,Real-time computing,Priority queue,Mathematical proof
DocType
Citations 
PageRank 
Conference
1
0.38
References 
Authors
16
6
Name
Order
Citations
PageRank
Sumesh Divakaran130.80
Deepak D'souza223917.90
Anirudh Kushwah310.38
Prahladavaradan Sampath4647.65
Nigamanth Sridhar513119.10
J. C. P. Woodcock651953.82