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.
Liste complète des métadonnées

https://hal.inria.fr/hal-01878100
Contributor : Xiaojie Guo <>
Submitted on : Thursday, September 20, 2018 - 4:21:39 PM
Last modification on : Thursday, October 11, 2018 - 8:48:04 AM
Document(s) archivé(s) le : Friday, December 21, 2018 - 4:19:21 PM

File

main.pdf
Files produced by the author(s)

Identifiers

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⟩

Share

Metrics

Record views

263

Files downloads

125