Verifying the Implementation of an Operating System Scheduler
Verifying the Implementation of an Operating System Scheduler
复制标题
验证操作系统调度程序的实现
DOI：
10.1109/tase.2009.58
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
S. Glesner
中科院分区：
文献类型：
--
作者：
Moritz Kleine;B. Bartels;Thomas Göthel;S. Glesner
在本文中，我们将验证低级代码的方法应用于实时操作系统BOSS的调度程序。我们在CSP-OZ中开发了它的高级规范，并展示了它执行BOSS调度策略。此外，我们提出了一个低级CSP M模型，该模型已经从其实现中半自动合成。使用自动FDR2改进检查器，我们证明了低级模型是调度程序的CSP- oz规范的CSP M编码的故障发散改进。首先，这意味着方法正在终止。其次，实现尊重其规范的前置和后置条件。第三，实现生成CSP-OZ规范所描述的时间表。我们打算用我们的方法检查BOSS的其他组成部分。另一个目标是扩展它，通过使用我们在Isabelle/HOL定理证明器[T]中对定时CSP的形式化来验证实时系统。Gothel and S. Glesner, 2009]。
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].