Contributions to Prosa

Two schedulability analyses for uniprocessor systems have been formalized and mechanically verified in Coq for:

  1. sporadic task sets scheduled according to the Time Division Multiple Access (TDMA) policy.
  2. periodic task sets with offsets scheduled according to the Fixed Priority Preemptive (FPP) policy.
  3. generic proof of Typical Worst-Case Analysis

This work builds on top of and enriches the Prosa library.

Comments are closed