Deductive Verification for Earliest Deadline First Scheduler Implementations

Daniel Kuhse, Junjie Shi, Jan Duy Thien Pham +4

Real-Time Operating Systems (RTOSes) rely on scheduler implementations to provide predictable task execution. For safety-critical systems, it is therefore not sufficient to reason…