Applying Rely-Guarantee Reasoning on Concurrent Memory Management and Mailbox in C/OS-II: A Case Study

Real-time operating systems (RTOSs) such as C/OS-II are critical components of many industrial systems, which makes it of vital importance to verify their correctness. However, earlier specifications for verification of RTOSs often do not explicitly specify the behavior of possible unbounded kernel service invocations. To address the problem, a new event-based modelling approach is recently proposed to treat the operating system as a concurrent reactive system (CRS). Besides, a respective parametric rely-guarantee style reasoning framework called PiCore is developed to verify such systems effectively. Witnessing the advancement, we conduct a case study to investigate the use of PiCore to compositionally verify two important entangled modules of a practical RTOS C/OS-II, i.e., the memory management module and the mailbox module. Several desirable safety properties regarding the memory pools and mailboxes are formally defined and proved with PiCore ( 2500 lines of specifications and proof scripts in Isabelle/HOL) based on a formal execution model considering the two modules simultaneously. We also discuss the shortcomings of PiCore for our case study and present possible improvement directions.