Project Page Index Table of Contents

# Library prosa.model.priority.rate_monotonic

Require Export prosa.model.priority.classes.
Require Export prosa.model.task.arrival.sporadic.

# Rate-Monotonic Fixed-Priority Policy

We define what it means for an abstract fixed-priority policy to behave as rate-monotonic.
Section RMPolicy.
Consider sporadic tasks.
Context {Task : TaskType} `{SporadicModel Task}.
A fixed-priority policy is rate-monotonic if it assigns higher priority to tasks with shorter minimum inter-arrival times, or periods.
Definition policy_is_RM (FP : FP_policy Task) :=
∀ tsk1 tsk2,
hep_task tsk1 tsk2
= (task_min_inter_arrival_time tsk1 ≤ task_min_inter_arrival_time tsk2).
End RMPolicy.