Formal Verification of a Timing Enforcer Implementation.

A timing enforcer is a scheduler that not only allocates CPU cycles to threads, but also uses timers to enforce time budgets. An approach for verifying safety properties of timing enforcers at the source code level is presented. We assume that the enforcer is implemented as a set of “enforcer” functions that are executed atomically on critical system-level events, such as the arrival and departure of jobs, and triggering of timers. The key idea is to express the safety property as an invariant, and prove that it is inductive across all the enforcer functions. A formal semantics of timing enforcers is presented, including the semantics of functions used to read the system clock and set timers. Using this semantics, the verification approach is presented, and its soundness proved. Further, the approach also takes into consideration the periodicity of tasks. It is validated by proving the correctness of the enforcement of CPU cycle budgets for tasks by the Zero-Slack Rate Monotonic (zsrm) scheduler, which is implemented in C as a Linux kernel module. The inductiveness of the necessary zsrm invariants is proved by expressing them as function contracts using the acsl specification language, and verifying the contracts using the frama-c tool.