Automated verification of the FreeRTOS scheduler in HIP/SLEEK

作者：Ferreira, Joao F; Gherghina, Cristian; He, Guanhua; Qin, Shengchao^*; Chin, Wei Ngan

来源：International Journal on Software Tools for Technology Transfer, 2014, 16(4): 381-397.

DOI：10.1007/s10009-014-0307-4

• FreeRTOS
• Separation logic
• Automated verification
• Operating systems
• Embedded systems
• Task scheduler
• 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 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 lemmasmake 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-8
• 单位深圳大学