Software Engineering Institute | Carnegie Mellon University
Software Engineering Institute | Carnegie Mellon University

Digital Library

Javascript is currently disabled for your browser. For an optimal search experience, please enable javascript.

Advanced Search

Basic Search

Content Type

Topics

Publication Date

Conference Paper

Contract-Based Verification of Timing Enforcers

  • October 2016
  • By Sagar Chaki4807, Dionisio de Niz3373
  • 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.
  • Publisher: Software Engineering Institute
  • Abstract

    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.

  • Download