The FLINT Project

Research

People

Publications

Software

Support

Links

Internal

Integrating Formal Schedulability Analysis into a Verified OS Kernel

Last modified: Sat Sep 7 19:53:50 2019 GMT.

CAV Artifact Evaluation

Authors

Xiaojie Guo
Maxime Lesourd
Mengqi Liu
Lionel Rieg
Zhong Shao

Abstract

Formal verification of real-time systems is attractive because these systems often perform critical operations. Unlike non real-time systems, latency and response time guarantees are of critical importance in this setting, as much as functional correctness. Nevertheless, formal verification of real-time OSes usually stops the scheduling analysis at the policy level: they only prove that the scheduler (or its abstract model) satisfies some scheduling policy. In this paper, we go further and connect together Prosa, a verified schedulability analyzer, and RT-CertiKOS, a verified single-core sequential real-time OS kernel. Thus, we get a more general and extensible schedulability analysis proof for RT-CertiKOS, as well a concrete implementation validating Prosa models. It also showcases that it is realistic to connect two completely independent formal developments in a proof assistant.

Published

In Proc. 31st International Conference on Computer Aided Verification (CAV 2019), New York, USA, Part II, LNCS 11562, pages 496-514, July 2019.
  • Conference Paper PDF

  • Copyright © 1996-2019 The FLINT Group <flint at cs dot yale dot edu>
    Yale University Department of Computer Science
    Validate this page
    colophon