A Generalized Digraph Model for Expressing Dependencies

Abstract : In the context of computer assisted verification of schedulability analyses, very expressive task models are useful to factorize the correctness proofs of as many analyses as possible. The digraph task model seems a good candidate due to its powerful expressivity. Alas, its ability to capture dependencies between arrival and execution times of jobs of different tasks is very limited. We propose here a task model that generalizes the digraph model and its corresponding analysis for fixed-priority scheduling with limited preemption. A task may generate several types of jobs, each with its own worst-case execution time, priority, non-preemptable segments and maximum jitter. We present the correctness proof of the analysis in a way amenable to its formalization in the Coq proof assistant. Our objective (still in progress) is to formally certify the analysis for that general model such that the correctness proof of a more specific (standard or novel) analysis boils down to specifying and proving its translation into our model. Furthermore, expressing many different analyses in a common framework paves the way for formal comparisons.
Type de document :
Communication dans un congrès
RTNS '18 - 26th International Conference on Real-Time Networks and Systems, Oct 2018, Chasseneuil-du-Poitou, France. pp.1-11, 〈10.1145/3273905.3273918〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01878100
Contributeur : Xiaojie Guo <>
Soumis le : jeudi 20 septembre 2018 - 16:21:39
Dernière modification le : jeudi 11 octobre 2018 - 08:48:04

Fichier

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

Identifiants

Citation

Pascal Fradet, Xiaojie Guo, Jean-François Monin, Sophie Quinton. A Generalized Digraph Model for Expressing Dependencies. RTNS '18 - 26th International Conference on Real-Time Networks and Systems, Oct 2018, Chasseneuil-du-Poitou, France. pp.1-11, 〈10.1145/3273905.3273918〉. 〈hal-01878100〉

Partager

Métriques

Consultations de la notice

78

Téléchargements de fichiers

30