The following results for real-time systems analysis are built on top of and enrich the Prosa library.
- Response time analysis of sporadic task sets scheduled according to the Time Division Multiple Access (TDMA) policy on a uniprocessor
- Response time analysis of periodic task sets with offsets scheduled according to the Fixed Priority Preemptive (FPP) policy on a uniprocessor
- A generic proof of Typical Worst-Case Analysis
- CertiCAN: A tool for the Coq certification of CAN analysis results