Library prosa.model.task.arrival.periodic

The Periodic Task Model

In the following, we define the classic Liu & Layland arrival process, i.e., the arrival process commonly known as the periodic task model, wherein the arrival times of consecutive jobs of a periodic task are separated by the task's period.

Task Model Parameter for Periods

Under the periodic task model, each task is characterized by its period, which we denote as task_period.

Model Validity

Next, we define the semantics of the periodic task model.
Consider any type of periodic tasks.
  Context {Task : TaskType} `{PeriodicModel Task}.

A valid periodic task has a non-zero period.
  Definition valid_period (tsk : Task) := task_period tsk > 0.

Next, consider any type of jobs stemming from these tasks ...
  Context {Job : JobType} `{JobTask Job Task} `{JobArrival Job}.

... and an arbitrary arrival sequence of such jobs.
  Variable arr_seq : arrival_sequence Job.

We say that a task respects the periodic task model if every job j (except the first one) has a predecessor j' that arrives exactly one task period before it.
  Definition respects_periodic_task_model (tsk : Task) :=
      arrives_in arr_seq j
      job_index arr_seq j > 0
      job_task j = tsk
        arrives_in arr_seq j'
        job_index arr_seq j' = job_index arr_seq j - 1
        job_task j' = tsk
        job_arrival j = job_arrival j' + task_period tsk.

Further, in the context of a set of periodic tasks, ...
  Variable ts : TaskSet Task.

... every task in the set must have a valid period ...
  Definition valid_periods := tsk : Task, tsk \in ts valid_period tsk.

... and all jobs of every task in a set of periodic tasks must respect the period constraint on arrival times.