Automated verification of the freeRTOS scheduler in HIP/SLEEK

Automated verification of operating system kernels is a challenging problem, partly due to the use of shared mutable data structures. In this paper, we show how we can automatically verify memory safety and functional correctness of the task scheduler component of the FreeRTOS kernel using the verif...

Full description

Bibliographic Details
Main Author: Ferreira, João Fernando (author)
Other Authors: Guanhua He (author), Shengchao Qin (author)
Format: conferencePaper
Language:eng
Published: 2012
Subjects:
Separation logic
Freertos
Verification
automated verification
embedded systems
HIP/SLEEK
operating systems
task scheduler
Online Access:http://hdl.handle.net/1822/38093
Country:Portugal
Oai:oai:repositorium.sdum.uminho.pt:1822/38093

Internet

http://hdl.handle.net/1822/38093

Similar Items