Work In Progress: Toward a Coq-certified Tool for the Schedulability Analysis of Tasks with Offsets

Abstract : This paper presents the first steps toward a formally proven tool for schedulability analysis of tasks with offsets. We formalize and verify the seminal response time analysis of Tindell by extending the Prosa proof library, which is based on the Coq proof assistant. Thanks to Coq’s extraction capabilities, this will allow us to easily obtain a certified analyzer. Additionally, we want to build a Coq certifier that can verify the correctness of results obtained using related (but uncertified), already existing analyzers. Our objective is to investigate the advantages and drawbacks of both approaches, namely the certified analysis and the certifier. The work described in this paper as well as its continuation is intended to enrich the Prosa library.
Type de document :
Communication dans un congrès
RTSS 2017 - IEEE Real-Time Systems Symposium, Dec 2017, Paris, France. IEEE, pp.1-3
Liste complète des métadonnées

Littérature citée [2 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01629288
Contributeur : Xiaojie Guo <>
Soumis le : mercredi 8 novembre 2017 - 11:22:47
Dernière modification le : vendredi 6 juillet 2018 - 10:08:02
Document(s) archivé(s) le : vendredi 9 février 2018 - 12:47:53

Fichier

offset_WiP.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01629288, version 1

Citation

Xiaojie Guo, Sophie Quinton, Pascal Fradet, Jean-François Monin. Work In Progress: Toward a Coq-certified Tool for the Schedulability Analysis of Tasks with Offsets. RTSS 2017 - IEEE Real-Time Systems Symposium, Dec 2017, Paris, France. IEEE, pp.1-3. 〈hal-01629288〉

Partager

Métriques

Consultations de la notice

260

Téléchargements de fichiers

79