search menu icon-carat-right cmu-wordmark

Contract-Based Verification of Timing Enforcers

Conference Paper
In this paper, the authors focus on proving the correctness of the budget enforcement that guarantees that no task τi executes beyond its W1 i. They present their approach and some preliminary results.

Software Engineering Institute


Contract-Based Verification of Timing Enforcers 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 con- tracts using the FRAMA-c tool.