Details

Autor(en) / Beteiligte

• Kleine, M.
• Bartels, B.
• Gothel, T.
• Glesner, S.

Titel

Verifying the Implementation of an Operating System Scheduler

Ist Teil von

• 2009 Third IEEE International Symposium on Theoretical Aspects of Software Engineering, 2009, p.285-286

Ort / Verlag

IEEE

Erscheinungsjahr

2009

Link zum Volltext

• IEEE_Xplore

Quelle

IEEE Xplore Digital Library

Beschreibungen/Notizen

• 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].