Contract-Based Verification of Timing Enforcers: [Extended Abstract]

A timing enforcer 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 entry functions that are executed atomically on critical system-level events, such as arrival and departure of periodic jobs. The key idea is to express the safety property as an invariant, and prove that it is inductive across all the entry functions. The approach is validated by proving correctness of the enforcement of CPU cycle budgets for tasks by a mixed-criticality scheduler called zsrm that is implemented in C. 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.