Titre :

pip_edf_scheduler

Auteur(s) :

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

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

Computer Science
Provable Security
Security
Formal Methods
Operating System
Scheduler
Scheduling
Real time scheduling
Real time

Discipline(s) HAL :

Informatique [cs]

Résumé en anglais : [en]

This repository holds the code and proofs of a formally verified, userland, job-based, earliest deadline first scheduler running on top of the Pip kernel. You can find more about the Pip protokernel at its website ...
Lire la suite >This repository holds the code and proofs of a formally verified, userland, job-based, earliest deadline first scheduler running on top of the Pip kernel. You can find more about the Pip protokernel at its website (https://pip.univ-lille.fr).This scheduler features a formally proven election function written in Gallina (the specification language of the Coq Proof Assistant).The repository also hold sources for a program (back-end) that acts as a simulation of the scheduler, that prints relevant information regarding the internal state of the election function.Lire moins >

Langue :

Anglais

Collections :

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

Source :

Harvested from HAL