Tasks system

Ramona is a realtime model-checker that generates an abstraction of the state-space of systems of preemptive tasks, with fixed priority and executing on a single processor. In the future, we plan to extend our approach to computation over multiple processors and with the addition of dependencies between tasks. We also plan to add a syntax for describing communication dependencies between tasks and to compute some timing properties, such as age delay.

In our setting, a task is defined by its period, its duration and possibly an offset defined as a (closed) time interval between two values, omin and omax. All these values are integers.

Below is an example of a simple task system with three tasks (task0, task1 and task2) with respective periods 10, 15 and 15. When omitted, offset are considered equal to zero (tasks are scheduled immediately after being activated).

#
# period, duration, offset_min, offset_max
#
10, 3, 1, 1
15, 2
15, 2

A task system is simply a list of task declarations. We consider that tasks are identified by their index on this list and that they are listed in their order of priority (hence task0 has higher priority over task1).

Our approach relies on the fact that durations are fixed. This constraint is not necessary for periods. Actually, we can view offsets as a way to model uncertainty on the periods (or as a poor man’s way to model jitter).

In our semantics, tasks can be in one of 4 possible states:

• ready (task is scheduled but is awaiting to start),

• run (task has started is computation, but it can be interrupted by higher-priority tasks),

• idle (task has finished and is awaiting the end of its period), and

• delay (that models the case when the processor is busy with a high-priority task but the task needs to start executing now).

The semantics of a single task is given by the state machine in Figure 2. A system is interpreted as the (parallel) composition of all its tasks.