# Library prosa.analysis.definitions.tardiness

Require Export prosa.analysis.definitions.schedulability.

# Tardiness

In the following section we define the notion of bounded tardiness, i.e., an upper-bound on the difference between the response time of any job of a task and its relative deadline.
Section Tardiness.
Consider any type of tasks and its deadline, ...
Context {Task : TaskType}.
Context `{TaskDeadline Task}.
... any type of jobs associated with these tasks, ...
Context {Job : JobType}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Context `{JobTask Job Task}.
... and any kind of processor state.
Context {PState : ProcessorState Job}.
Further, consider any job arrival sequence...
Variable arr_seq : arrival_sequence Job.
...and any schedule of these jobs.
Variable sched : schedule PState.
Let tsk be any task that is to be analyzed.
Variable tsk : Task.
Then, we say that B is a tardiness bound of tsk in this schedule ...
Variable B : duration.
... iff any job j of tsk in the arrival sequence has completed no more that B time units after its deadline.
Definition task_tardiness_is_bounded arr_seq sched tsk B :=
task_response_time_bound arr_seq sched tsk (task_deadline tsk + B).
End Tardiness.