• English
    • français
  • Help
  •  | 
  • Contact
  •  | 
  • About
  •  | 
  • Login
  • HAL portal
  •  | 
  • Pages Pro
  • EN
  •  / 
  • FR
View Item 
  •   LillOA Home
  • Liste des unités
  • Centre de Recherche en Informatique, Signal et Automatique de Lille (CRIStAL) - UMR 9189
  • View Item
  •   LillOA Home
  • Liste des unités
  • Centre de Recherche en Informatique, Signal et Automatique de Lille (CRIStAL) - UMR 9189
  • View Item
JavaScript is disabled for your browser. Some features of this site may not work without it.

A Formal Correctness Proof for an EDF ...
  • BibTeX
  • CSV
  • Excel
  • RIS

Document type :
Communication dans un congrès avec actes
DOI :
10.1109/RTAS54340.2022.00030
Title :
A Formal Correctness Proof for an EDF Scheduler Implementation
Author(s) :
Vanhems, Florian [Auteur]
Rusu, Vlad [Auteur] refId
Analyse symbolique et conception orientée composants pour des systèmes embarqués temps-réel modulaires [SYCOMORES]
Nowak, David [Auteur] refId

Grimaud, Gilles [Auteur] refId
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
Files
Thumbnail
  • https://hal.inria.fr/hal-03671598v2/document
  • Open access
  • Access the document
Université de Lille

Mentions légales
Université de Lille © 2017