Title :

A Formal Correctness Proof for an EDF Scheduler Implementation

Author(s) :

Vanhems, Florian [Auteur]
Rusu, Vlad [Auteur]
Analyse symbolique et conception orientée composants pour des systèmes embarqués temps-réel modulaires [SYCOMORES]
Nowak, David [Auteur]

Grimaud, Gilles [Auteur]

Conference title :

RTAS 2022: 28th IEEE Real-Time and Embedded Technology and Applications Symposium

City :

Milan

Country :

Italie

Start date of the conference :

2022-05-04

Book title :

Proc. 28th IEEE Real-Time and Embedded Technology and Applications Symposium

English keyword(s) :

scheduler
EDF
job
proof
correction
implementation
coq
verification
formal
refinement
monad
real-time
TCB
shallow embedding

HAL domain(s) :

Informatique [cs]/Systèmes embarqués

English abstract : [en]

The scheduler is a critical piece of software inreal-time systems. A failure in the scheduler can have seriousconsequences; therefore, it is important to provide strong cor-rectness guarantees for it. In this paper we ...
Show more >The scheduler is a critical piece of software inreal-time systems. A failure in the scheduler can have seriousconsequences; therefore, it is important to provide strong cor-rectness guarantees for it. In this paper we propose a formalproof methodology that we apply to an Earliest Deadline First(EDF) scheduler. It consists first in proving the correctness of theelection function algorithm and then lifting this proof up to theimplementation through refinements. The proofs are formalizedin the Coq proof assistant, ensuring that they are free of humanerrors and that all cases are considered. Our methodology isgeneral enough to be applied to other schedulers or other typesof system code. To the best of our knowledge, this is the first timethat an implementation of EDF applicable to arbitrary sequencesof jobs has been proven correct.Show less >

Language :

Anglais

Peer reviewed article :

Oui

Audience :

Internationale

Popular science :

Non

ANR Project :

Tiny, PrivAte, Proved & isolaTed

Collections :

• Centre de Recherche en Informatique, Signal et Automatique de Lille (CRIStAL) - UMR 9189

Source :

Harvested from HAL