Proof of OS Scheduling Behavior in the Presence of Interrupt-Induced Concurrency
ITP, pp. 52-68, 2016.
We present a simple yet scalable framework for formal reasoning and machine-assisted proof of interrupt-driven concurrency in operating-system code, and use it to prove the principal scheduling property of the embedded, real-time eChronos OS: that the running task is always the highest-priority runnable task. The key differentiator of thi...More
Full Text (Upload PDF)
PPT (Upload PPT)