# 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 arrival curves.
Section DemandBoundFunction.
Consider any type of tasks.
Context {Task : TaskType}.
Suppose each task is characterized by a WCET, a relative deadline, and an arrival curve.
Context `{TaskCost Task} `{TaskDeadline Task} `{MaxArrivals 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.