Title :

pip_edf_scheduler

Author(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]

English keyword(s) :

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

HAL domain(s) :

Informatique [cs]

English abstract : [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 ...
Show more >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.Show less >

Language :

Anglais

Collections :

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

Source :

Harvested from HAL