Skip to Main content Skip to Navigation
Conference papers

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 metadata

Cited literature [33 references]  Display  Hide  Download
Contributor : Sophie Quinton Connect in order to contact the contributor
Submitted on : Wednesday, October 24, 2018 - 3:52:08 PM
Last modification on : Wednesday, November 3, 2021 - 6:45:55 AM
Long-term archiving on: : Friday, January 25, 2019 - 3:20:44 PM


Files produced by the author(s)


  • HAL Id : hal-01903752, version 1


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⟩



Les métriques sont temporairement indisponibles