Automated verification of the FreeRTOS scheduler in Hip/Sleek

Joao Ferreira, Cristian Gherghina, Guanhua He, Shengchao Qin, Wei-Ngan Chin

Research output: Contribution to journalArticle

147 Downloads (Pure)

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.
Original languageEnglish
Pages (from-to)-
JournalInternational Journal on Software Tools for Technology Transfer
DOIs
Publication statusPublished - 18 Mar 2014

Fingerprint Dive into the research topics of 'Automated verification of the FreeRTOS scheduler in Hip/Sleek'. Together they form a unique fingerprint.

  • Cite this