Verifying the Implementation of an Operating System Scheduler

In this paper, we applied our approach for verifying low-level code to the scheduler of the real-time operating system BOSS. We developed its high-level specification in CSP-OZ and showed that it enforces the BOSS scheduling strategy. Furthermore, we presented a low-level CSP_M model, which has been semi-automatically synthesized from its implementation. Using the automatic FDR2 refinement checker, we proved that the low-level model is a failures-divergence refinement of the CSP_M encoding of the scheduler´s CSP-OZ specification. First, this means that the methods are terminating. Second, the implementation respects the pre- and post-conditions of its specification. Third, the implementation produces exactly the schedules that are described by the CSP-OZ specification. We intend to examine other components of BOSS using our approach. Another objective is to extend it to enable the verification of real-time systems by using our formalization of Timed CSP in the Isabelle/HOL theorem prover [T. Gothel and S. Glesner, 2009].