Titre :

A Formal Correctness Proof for an EDF Scheduler Implementation

Auteur(s) :

Vanhems, Florian [Auteur]
Université de Lille
Rusu, Vlad [Auteur]
Analyse symbolique et conception orientée composants pour des systèmes embarqués temps-réel modulaires [SYCOMORES]
Nowak, David [Auteur]
Extra Small Extra Safe [2XS]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Centre National de la Recherche Scientifique [CNRS]
Grimaud, Gilles [Auteur]
Université de Lille

Titre de la manifestation scientifique :

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

Ville :

Milan

Pays :

Italie

Date de début de la manifestation scientifique :

2022-05-04

Titre de l’ouvrage :

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

Mot(s)-clé(s) en anglais :

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

Discipline(s) HAL :

Informatique [cs]/Systèmes embarqués

Résumé en anglais : [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 ...
Lire la suite >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.Lire moins >

Langue :

Anglais

Comité de lecture :

Oui

Audience :

Internationale

Vulgarisation :

Non

Projet ANR :

Tiny, PrivAte, Proved & isolaTed

Collections :

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

Source :

Harvested from HAL