Library prosa.analysis.definitions.demand_bound_function

Require Export prosa.analysis.definitions.request_bound_function.

Demand Bound Function (DBF)

Here we define Baruah et al.'s classic notion of a demand bound function, generalized to arbitrary request-bound functions.
Section DemandBoundFunction.
Consider any type of tasks.
  Context {Task : TaskType}.

Suppose each task is characterized by a relative deadline and an RBF.
  Context `{TaskDeadline Task} `{MaxRequestBound Task}.

A task's DBF is its request-bound function (RBF) shifted by task_deadline tsk - 1 time units.
  Definition task_demand_bound_function (tsk : Task) (delta : duration) :=
    let delta' := delta - (task_deadline tsk - 1) in
      task_request_bound_function tsk delta'.

A task set's total demand bound function is simply the sum of each task's DBF.
  Definition total_demand_bound_function (ts : seq Task) (delta : duration) :=
    \sum_(tsk <- ts) task_demand_bound_function tsk delta.

End DemandBoundFunction.