Integrating Formal Schedulability Analysis into a Verified OS Kernel - Archive ouverte HAL Access content directly
Conference Papers Year : 2019

Integrating Formal Schedulability Analysis into a Verified OS Kernel

(1) , (2) , (3) , (2, 3) , (3)
1
2
3
Maxime Lesourd
Lionel Rieg

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.

Dates and versions

hal-02289494 , version 1 (16-09-2019)

Identifiers

Cite

Xiaojie Guo, Maxime Lesourd, Mengqi Liu, Lionel Rieg, Zhong Shao. Integrating Formal Schedulability Analysis into a Verified OS Kernel. Computer Aided Verification, Jul 2019, New York, United States. pp.496-514, ⟨10.1007/978-3-030-25543-5_28⟩. ⟨hal-02289494⟩
130 View
0 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More