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.

A valid periodic task has a non-zero period.

Further, in the context of a set of periodic tasks, ...

... every task in the set must have a valid period.

Next, consider any type of jobs stemming from these tasks ...

... and an arbitrary arrival sequence of such jobs.

We say that a task respects the periodic task model if the arrivals of its jobs in the arrival sequence are separated by integer multiples of the period.

Given two different jobs j and j' ...

...that belong to the arrival sequence...

... and that stem from the given task, ...

... if [j] arrives no later than [j'] ...,

... then the arrivals of [j] and [j'] are separated by an integer multiple of [task_period tsk].

Every task in a set of periodic tasks must satisfy the above criterion.

Treating Periodic Tasks as Sporadic Tasks

Since the periodic-arrivals assumption is stricter than the sporadic-arrivals assumption (i.e., any periodic arrival sequence is also a valid sporadic arrivals sequence), it is sometimes convenient to apply analyses for sporadic tasks to periodic tasks. We therefore provide an automatic "conversion" of periodic tasks to sporadic tasks, i.e., we tell Coq that it may use a periodic task's [task_period] parameter also as the task's minimum inter-arrival time [task_min_inter_arrival_time] parameter.

Any type of periodic tasks ...

... and their corresponding jobs ...

... may be interpreted as a type of sporadic tasks by using each task's period as its minimum inter-arrival time ...

... such that the model interpretation is valid, both w.r.t. the minimum inter-arrival time parameter ...

... and the separation of job arrivals.

For convenience, we state these obvious correspondences also at the level of entire task sets.