Two schedulability analyses for uniprocessor systems have been formalized and mechanically verified in Coq for:
- sporadic task sets scheduled according to the Time Division Multiple Access (TDMA) policy.
- periodic task sets with offsets scheduled according to the Fixed Priority Preemptive (FPP) policy.
- generic proof of Typical Worst-Case Analysis
This work builds on top of and enriches the Prosa library.