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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [33 references]  Display  Hide  Download

https://hal.inria.fr/hal-01903752
Contributor : Sophie Quinton <>
Submitted on : Wednesday, October 24, 2018 - 3:52:08 PM
Last modification on : Monday, November 12, 2018 - 12:04:01 PM
Long-term archiving on : Friday, January 25, 2019 - 3:20:44 PM

File

main.pdf
Files produced by the author(s)

Identifiers

  • 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⟩

Share

Metrics

Record views

203

Files downloads

359