A Generic Coq Proof of Typical Worst-Case Analysis

Abstract : This paper presents a generic proof of Typical Worst-Case Analysis (TWCA), an analysis technique for weakly-hard real-time uniprocessor systems. TWCA was originally introduced for systems with fixed priority preemptive (FPP) schedulers and has since been extended to fixed-priority nonpreemptive (FPNP) and earliest-deadline-first (EDF) schedulers. Our generic analysis is based on an abstract model that characterizes the exact properties needed to make TWCA applicable to any system model. Our results are formalized and checked using the Coq proof assistant along with the Prosa schedulability analysis library. Our experience with formalizing real-time systems analyses shows that this is not only a way to increase confidence in our claimed results: The discipline required to obtain machine checked proofs helps understanding the exact assumptions required by a given analysis, its key intermediate steps and how this analysis can be generalized.
Type de document :
Communication dans un congrès
RTSS 2018 - 39th IEEE Real-Time Systems Symposium, Dec 2018, Nashville, United States. pp.1-12
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01903752
Contributeur : Sophie Quinton <>
Soumis le : mercredi 24 octobre 2018 - 15:52:08
Dernière modification le : lundi 12 novembre 2018 - 12:04:01
Document(s) archivé(s) le : vendredi 25 janvier 2019 - 15:20:44

Fichier

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

Identifiants

  • HAL Id : hal-01903752, version 1

Citation

Pascal Fradet, Maxime Lesourd, Jean-François Monin, Sophie Quinton. A Generic Coq Proof of Typical Worst-Case Analysis. RTSS 2018 - 39th IEEE Real-Time Systems Symposium, Dec 2018, Nashville, United States. pp.1-12. 〈hal-01903752〉

Partager

Métriques

Consultations de la notice

121

Téléchargements de fichiers

147