Library probsa.rt.model.WCET
(* --------------------------------- Prosa ---------------------------------- *)
Require Export prosa.model.task.concept.
(* --------------------------------- ProBsa --------------------------------- *)
From probsa.rt.behavior Require Export job.
(* ---------------------------------- Main ---------------------------------- *)
Require Export prosa.model.task.concept.
(* --------------------------------- ProBsa --------------------------------- *)
From probsa.rt.behavior Require Export job.
(* ---------------------------------- Main ---------------------------------- *)
... any type of tasks with costs defined by a function
task_cost, ...
... and any type of jobs associated with these tasks. Assume
that the jobs have probabilistic costs defined by job_cost.
We say that task_cost is a WCET iff for any job j and its task
job_task j the two conditions hold:
(i) The job's cost is less than or equal to the task's cost in all
evolutions ω ∈ Ω. The statement uses the odflt0 function to
safely extract the value of job_cost j, or fallback to zero if
job_cost j is ⊥ for the given ω.
(ii) There exists an evolution ω such that job_cost j exactly
matches the task's cost in ω.