Verifying the Implementation of an Operating System Scheduler

摘要：

In this paper, we present a case study on verifying the implementation of the scheduler of the real-time operating system BOSS. It illustrates our approach to verifying low-level software systems, which is based on the automatic generation of a low-level CSP model from the LLVM intermediate representation (IR) of a program. To prove the implementation correct, it must be shown that the low-level model conforms to a high-level specification of the system. To this end, we use the FDR2 refinement checker. After giving the formal background, we informally introduce the scheduler, present its specification in CSP-OZ and show how the low-level model is obtained from the LLVM IR.

作者: Moritz Kleine Bj(o)rn Bartels Thomas G(o)thel Sabine Glesner

作者单位: Technical University of Berlin Institute for Software Engineering and Theoretical Computer Science

会议类型: 国际会议

会议名称: Third International Symposium on Theoretical Aspects of Software Engineering TASE 2009(第三届软件工程理论国际研讨会)

会议地点: 天津

会议语种:英文

页码: 285-286

在线出版日期: 2009-07-29（万方平台首次上网日期，不代表论文的发表时间）