TY - GEN
T1 - Verifying FreeRTOS' Cyclic Doubly Linked List Implementation
T2 - 20th International Conference on Engineering of Complex Computer Systems, ICECCS 2015
AU - Sanan, David
AU - Yang, Liu
AU - Yongwang, Zhao
AU - Zhenchang, Xing
AU - Hinchey, Mike
N1 - Publisher Copyright:
© 2015 IEEE.
PY - 2016/1/15
Y1 - 2016/1/15
N2 - In order to facilitate proof of correctness, micro-kernels are based on simplicity, providing an application only with the minimal set of features it needs in order to to work. However, simplicity alone does not guarantee the absence of bugs and software errors, and the complexity of an OS often makes such problems difficult to find and fix. In this work, we prove the functional correctness of an abstract model for the C implementation of the cyclic linked list in the real-time micro-kernel FreeRTOS, which is used in the FreeRTOS scheduler, its correctness being of critical importance for the real-time properties of FreeRTOS. The formal specification of the functional properties of FreeRTOS also provides a guide for a correct use of the functions that the implementation provides, since it lacks checks on the data. Additionally, we prove the correctness of the machine code resulting from compiling the implementation targeting the ARM architecture. Following a verification approach based on refinement, we first construct the abstract model of the implementation, where we prove both the cyclic linked list invariant and the correctness of the implementation behaviour for any list in the heap using separation logic. Second, we leverage existing machine code verification frameworks to get a HOL model of the FreeRTOS linked list compiled machine code, and we apply forward simulation to prove that such a machine code model refines the abstract model, and therefore satisfies the properties already proven over the specification.
AB - In order to facilitate proof of correctness, micro-kernels are based on simplicity, providing an application only with the minimal set of features it needs in order to to work. However, simplicity alone does not guarantee the absence of bugs and software errors, and the complexity of an OS often makes such problems difficult to find and fix. In this work, we prove the functional correctness of an abstract model for the C implementation of the cyclic linked list in the real-time micro-kernel FreeRTOS, which is used in the FreeRTOS scheduler, its correctness being of critical importance for the real-time properties of FreeRTOS. The formal specification of the functional properties of FreeRTOS also provides a guide for a correct use of the functions that the implementation provides, since it lacks checks on the data. Additionally, we prove the correctness of the machine code resulting from compiling the implementation targeting the ARM architecture. Following a verification approach based on refinement, we first construct the abstract model of the implementation, where we prove both the cyclic linked list invariant and the correctness of the implementation behaviour for any list in the heap using separation logic. Second, we leverage existing machine code verification frameworks to get a HOL model of the FreeRTOS linked list compiled machine code, and we apply forward simulation to prove that such a machine code model refines the abstract model, and therefore satisfies the properties already proven over the specification.
KW - Formal methods
KW - Machine Code verification
KW - Microkernel Verification
KW - Theorem Proving verification
UR - http://www.scopus.com/inward/record.url?scp=84964848642&partnerID=8YFLogxK
U2 - 10.1109/ICECCS.2015.23
DO - 10.1109/ICECCS.2015.23
M3 - Conference contribution
AN - SCOPUS:84964848642
T3 - Proceedings of the IEEE International Conference on Engineering of Complex Computer Systems, ICECCS
SP - 120
EP - 129
BT - Proceedings - 2015 20th International Conference on Engineering of Complex Computer Systems, ICECCS 2015
PB - Institute of Electrical and Electronics Engineers Inc.
Y2 - 9 December 2015 through 11 December 2015
ER -