Automated verification of the FreeRTOS scheduler in Hip/Sleek

Hdl Handle:
http://hdl.handle.net/10149/594914
Title:
Automated verification of the FreeRTOS scheduler in Hip/Sleek
Authors:
Ferreira, J. F. (João); Gherghina, C. (Cristian); He, G. (Guanhua); Qin, S. (Shengchao); Chin, W. (Wei-Ngan)
Affiliation:
Teesside University, Digital Futures Institute
Citation:
Ferreira, J. F. (João); Gherghina, C. (Cristian); He, G. (Guanhua); Qin, S. (Shengchao); Chin, W. (Wei-Ngan) (2014) 'Automated verification of the FreeRTOS scheduler in Hip/Sleek' International Journal on Software Tools for Technology Transfer; 16 (4): 381-397.
Publisher:
Springer
Journal:
International Journal on Software Tools for Technology Transfer
Issue Date:
18-Mar-2014
URI:
http://hdl.handle.net/10149/594914
DOI:
10.1007/s10009-014-0307-4
Additional Links:
http://link.springer.com/10.1007/s10009-014-0307-4; http://joaoff.com/publications/2014/freertos-verification/2014-STTT-Ferreira-FreeRTOS.pdf
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.
Type:
Article
Language:
en
ISSN:
1433-2779; 1433-2787
Rights:
Author can archive post-print (ie final draft post-refereeing) subject to 12 months embargo.For full details see http://www.sherpa.ac.uk/romeo [Accessed 26/01/2016]

Full metadata record

DC FieldValue Language
dc.contributor.authorFerreira, J. F. (João)en
dc.contributor.authorGherghina, C. (Cristian)en
dc.contributor.authorHe, G. (Guanhua)en
dc.contributor.authorQin, S. (Shengchao)en
dc.contributor.authorChin, W. (Wei-Ngan)en
dc.date.accessioned2016-01-26T15:39:52Zen
dc.date.available2016-01-26T15:39:52Zen
dc.date.issued2014-03-18en
dc.identifier.citationInternational Journal on Software Tools for Technology Transfer; 16 (4): 381-397.en
dc.identifier.issn1433-2779en
dc.identifier.issn1433-2787en
dc.identifier.doi10.1007/s10009-014-0307-4en
dc.identifier.urihttp://hdl.handle.net/10149/594914en
dc.description.abstractAutomated 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.en
dc.language.isoenen
dc.publisherSpringeren
dc.relation.urlhttp://link.springer.com/10.1007/s10009-014-0307-4en
dc.relation.urlhttp://joaoff.com/publications/2014/freertos-verification/2014-STTT-Ferreira-FreeRTOS.pdfen
dc.rightsAuthor can archive post-print (ie final draft post-refereeing) subject to 12 months embargo.For full details see http://www.sherpa.ac.uk/romeo [Accessed 26/01/2016]en
dc.titleAutomated verification of the FreeRTOS scheduler in Hip/Sleeken
dc.typeArticleen
dc.contributor.departmentTeesside University, Digital Futures Instituteen
dc.identifier.journalInternational Journal on Software Tools for Technology Transferen
or.citation.harvardFerreira, J. F. (João); Gherghina, C. (Cristian); He, G. (Guanhua); Qin, S. (Shengchao); Chin, W. (Wei-Ngan) (2014) 'Automated verification of the FreeRTOS scheduler in Hip/Sleek' International Journal on Software Tools for Technology Transfer; 16 (4): 381-397.en
dc.description.fundingThis work was supported in part by the EPSRC project EP/G042322 and NNSFC project 61373033en
All Items in TeesRep are protected by copyright, with all rights reserved, unless otherwise indicated.