Commit 425ff442 authored by Martin PORTALIER's avatar Martin PORTALIER

Update readme.md

parent 6538d5b7
Pipeline #19285 failed with stages
in 2 minutes and 13 seconds
# Formal proof for maximisation of job response time in real time systems
Those files provide a proof that, under some hypothesis, if the workload bound has a fixpoint,
then it bounds the job response time and there exists a case where it is reached.
Those files provide a proof that, considering one job, if the workload bound has a fixpoint
then it bounds the job response time of the considered job and there exists a case where it is reached.
This proof is supposed to be as direct as possible.
......@@ -21,10 +21,10 @@ This proof supposes that :
- the arrival sequence model is sporadic (there exists a task minimal period)
- the deadline are implicit (the task deadline is equal to the task minimal period)
- the policy is with fixed preemptives priorities
- the system is schedulable (all jobs completes before their deadline)
- the system is schedulable (all jobs complete before their deadline)
Then the main hypothesis :
their exists a fixpoint for the workload bound, and the smallest one is reached.
their exists a fixpoint for the workload bound.
WARNING : A tricky hypothesis supposes that all jobs terminate.
I give some ideas to prove it in the section "To go further".
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment