Please use this identifier to cite or link to this item: https://doi.org/10.1007/s10009-014-0307-4
Title: Automated verification of the FreeRTOS scheduler in Hip/Sleek
Authors: Ferreira, J.F.
Gherghina, C.
He, G.
Qin, S.
Chin, W.-N. 
Keywords: Automated verification
Embedded systems
FreeRTOS
HIP/SLEEK
Operating systems
Separation logic
Task scheduler
Issue Date: 18-Mar-2014
Citation: Ferreira, J.F., Gherghina, C., He, G., Qin, S., Chin, W.-N. (2014-03-18). Automated verification of the FreeRTOS scheduler in Hip/Sleek. International Journal on Software Tools for Technology Transfer. ScholarBank@NUS Repository. https://doi.org/10.1007/s10009-014-0307-4
Abstract: 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 properties of the task scheduler component of the FreeRTOS kernel using the verification system Hip/Sleek. We show how some of Hip/Sleek features such as user-defined predicates and lemmas make the specifications highly expressive and the verification process viable. To the best of our knowledge, this is the first code-level verification of memory safety and functional correctness properties of the FreeRTOS scheduler. The outcome of our experiment confirms that Hip/Sleek can indeed be used to verify code that is used in production. Moreover, since the properties that we verify are quite general, we envisage that the same approach can be adopted to verify components of other operating systems. © 2014 Springer-Verlag Berlin Heidelberg.
Source Title: International Journal on Software Tools for Technology Transfer
URI: http://scholarbank.nus.edu.sg/handle/10635/123997
ISSN: 14332779
DOI: 10.1007/s10009-014-0307-4
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.

SCOPUSTM   
Citations

19
checked on Feb 21, 2020

WEB OF SCIENCETM
Citations

12
checked on Feb 21, 2020

Page view(s)

55
checked on Feb 22, 2020

Google ScholarTM

Check

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.