Add TDMA policy and RTA for TDMA

.gitignore

@@ -5,3 +5,8 @@
 *.aux
 Makefile*
 _CoqProject
+*.crashcoqide
+*.v#
+*.cache
+*~
+*.orig

analysis/uni/basic/tdma_rta_theory.v

+Require Import  rt.util.all rt.util.tactics_gr
+                rt.model.arrival.basic.job
+                rt.model.arrival.basic.task_arrival
+                rt.model.schedule.uni.schedulability
+                rt.model.schedule.uni.schedule_of_task 
+                rt.model.schedule.uni.response_time
+                rt.analysis.uni.basic.tdma_wcrt_analysis.
+Require Import  rt.model.schedule.uni.basic.platform_tdma
+                rt.model.schedule.uni.end_time.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div.
+
+Set Bullet Behavior "Strict Subproofs".
+
+Module ResponseTimeAnalysisTDMA.
+  
+  Import Job  TaskArrival ScheduleOfTask  ResponseTime Platform_TDMA end_time Schedulability
+        WCRT_OneJobTDMA.
+
+  (* In this section, we establish that the computed value WCRT of the exact response-time analysis
+     yields an upper bound on the response time of a task under TDMA scheduling policy on an uniprocessor, 
+     assuming that such value is no larger than the task period. *)
+
+  Section ResponseTimeBound.
+
+    (** System model *)
+    Context {sporadic_task: eqType}.
+    Variable task_cost: sporadic_task -> time.
+    Variable task_period: sporadic_task -> time.
+    Variable task_deadline: sporadic_task -> time.
+
+    Context {Job: eqType}.
+    Variable job_arrival: Job -> time.
+    Variable job_cost: Job -> time.
+    Variable job_deadline: Job -> time.
+    Variable job_task: Job -> sporadic_task.
+
+    (* Consider any arrival sequence... *)
+    Variable arr_seq: arrival_sequence Job.
+    Hypothesis H_arrival_times_are_consistent:
+      arrival_times_are_consistent job_arrival arr_seq.
+    Hypothesis H_sporadic_tasks:
+    sporadic_task_model task_period job_arrival job_task arr_seq.
+
+    (* ...and any uniprocessor... *)
+    Variable sched: schedule Job.
+    (* ... where jobs do not execute before their arrival times nor after completion. *)
+    Hypothesis H_jobs_must_arrive_to_execute:
+      jobs_must_arrive_to_execute job_arrival sched.
+    Hypothesis H_completed_jobs_dont_execute:
+      completed_jobs_dont_execute job_cost sched.
+
+    (* Consider any TDMA slot assignment... *)
+    Variable task_time_slot: TDMA_slot sporadic_task.
+    (* ... and any slot order. *)
+    Variable slot_order: TDMA_slot_order sporadic_task.
+
+    (* Consider any task set ts. *)
+    Variable ts: {set sporadic_task}.
+    Hypothesis H_valid_task_parameters:
+    valid_sporadic_taskset task_cost task_period task_deadline ts.
+
+    (* Consider any task in task set. *)
+    Variable tsk:sporadic_task.
+    Hypothesis H_task_in_task_set: tsk \in ts.
+
+    (* For simplicity, let us use local names for some definitions and refer them to local variables. *)
+    (* Recall definition: whether a job can be scheduled at time t *)
+    Let is_scheduled_at j t:= 
+      scheduled_at sched j t.
+    (* Recall definition: whether a task is in its own time slot at time t *)
+    Let in_time_slot_at j t:= 
+        Task_in_time_slot ts slot_order (job_task j) task_time_slot t.
+
+   (* Recall the definition of response-time bound. *)
+    Let response_time_bounded_by :=
+      is_response_time_bound_of_task job_arrival job_cost job_task arr_seq sched. 
+
+    (* Let (RT j) denote the computed response-time of job j according to the TDMA analysis.
+       Note that this computation assumes that there is only one pending job of each task.
+       Still, this assumption doesn't break the generality of the proof. There cannot be
+       multiple jobs of the same task because:
+       (a) assumption: the computed value WCRT is bounded by its task's period; and
+       (b) the lemma: "jobs_finished_before_WCRT" in file tdma_wcrt_analysis.v. *)
+    Hypothesis WCRT_le_period:
+      WCRT task_cost task_time_slot ts tsk <= task_period tsk.
+    Let RT j:= job_response_time_tdma_in_at_most_one_job_is_pending job_arrival job_cost
+         task_time_slot slot_order ts tsk j.
+
+    (* Next, recall the definition of deadline miss of tasks and jobs. *)
+    Let no_deadline_missed_by_task :=
+      task_misses_no_deadline job_arrival job_cost job_deadline job_task arr_seq sched.
+    Let no_deadline_missed_by_job :=
+      job_misses_no_deadline job_arrival job_cost job_deadline sched.
+
+    (* Then, we define a valid TDMA bound. *)
+    (* Bound is valid bound iff it is less than or equal to task's deadline *)
+    Definition is_valid_tdma_bound bound :=
+         (bound <= task_deadline tsk).
+
+    (* Now, let's assume that the schedule respects TDMA scheduling policy... *)
+    Hypothesis TDMA_policy:
+      Respects_TDMA_policy job_arrival job_cost job_task arr_seq sched ts task_time_slot slot_order.
+
+    (* ..., that task time slot is valid... *)
+    Hypothesis H_valid_time_slot:
+      is_valid_time_slot tsk task_time_slot.
+
+    (* ... and that any job in arrival sequence is a valid job. *)
+    Hypothesis H_valid_job_parameters:
+      forall j, arrives_in arr_seq j ->
+        valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
+
+    (* Assume that job cost is less than or equal to its task cost. *)
+    Hypothesis H_job_cost_le_task_cost: 
+      forall j, arrives_in arr_seq j ->
+      job_cost_le_task_cost task_cost job_cost job_task j.
+
+    (* Let BOUND be the computed WCRT of tsk. *)
+    Let BOUND := WCRT task_cost task_time_slot ts tsk.
+
+    (** Two basic lemmas  *)
+    (* Having assumed that the computed BOUND <= task_period tsk, we first prove that
+       any job of task tsk must have completed by its period. *)
+    Lemma any_job_completed_before_period:
+      forall j,
+        arrives_in arr_seq j ->
+        job_task j = tsk ->
+        completed_by job_cost sched j (job_arrival j + task_period  (job_task j) ).
+    Proof.
+      intros j [t ARR]. generalize dependent j.
+      induction t as [ t IHt ] using (well_founded_induction lt_wf).
+      case t eqn:GT;intros. 
+      - have INJ: arrives_in arr_seq j by exists 0.
+        (apply completion_monotonic with (t0:=job_arrival j + WCRT task_cost task_time_slot ts tsk )
+        ;trivial;try by rewrite leq_add2l H); apply job_completed_by_WCRT
+        with (task_deadline0:=task_deadline)
+                 (arr_seq0:=arr_seq)(job_deadline0:=job_deadline)
+                 (job_task0:=job_task)(slot_order0:=slot_order);eauto 2.
+        intros. apply H_arrival_times_are_consistent in ARR. ssromega.
+      - have INJ: arrives_in arr_seq j by exists n.+1.
+        apply completion_monotonic 
+          with (t0:=job_arrival j + WCRT task_cost task_time_slot ts tsk);auto.
+        by rewrite leq_add2l H. apply job_completed_by_WCRT
+        with (task_deadline0:=task_deadline)
+                 (arr_seq0:=arr_seq)(job_deadline0:=job_deadline)
+                 (job_task0:=job_task)(slot_order0:=slot_order);auto. 
+        intros.
+        have PERIOD: job_arrival j_other + task_period (job_task j_other)<= job_arrival j.
+        apply H_sporadic_tasks;auto. case (j==j_other)eqn: JJ;move/eqP in JJ;last auto.
+        have JO:job_arrival j_other = job_arrival j by f_equal. ssromega.
+        apply completion_monotonic with (t0:= job_arrival j_other +
+           task_period (job_task j_other)); auto.
+        have ARRJ: job_arrival j = n.+1 by auto.
+        apply (IHt (job_arrival j_other));auto. ssromega.
+        destruct H0 as [tj AAJO]. have CONSIST: job_arrival j_other =tj by auto.
+        by subst. by subst.
+    Qed.
+
+    (* Based on the lemma above and the fact that jobs arrive sporadically, we can conclude that
+       all the previous jobs of task tsk must have completed before the analyzed job j. *)
+    Lemma all_previous_jobs_of_same_task_completed :
+      forall j j_other,
+        arrives_in arr_seq j ->
+        job_task j = tsk ->
+        arrives_in arr_seq j_other ->
+        job_task j = job_task j_other ->
+        job_arrival j_other < job_arrival j ->
+        completed_by job_cost sched j_other (job_arrival j).
+    Proof.
+      intros.
+      have PERIOD: job_arrival j_other + task_period (job_task j_other)<= job_arrival j.
+      apply H_sporadic_tasks;auto. case (j==j_other)eqn: JJ;move/eqP in JJ;last auto. 
+      have JO:job_arrival j_other = job_arrival j by f_equal. ssromega.
+      apply completion_monotonic with (t:=job_arrival j_other + task_period (job_task j_other));auto.
+      apply any_job_completed_before_period;auto. by subst.
+    Qed.
+
+    (** Main Theorem *)
+    (* Therefore, we proved that the reponse time of task tsk is bouned by the 
+       BOUND i.e., the computed value WCRT according to TDMA scheduling policy on an uniprocessor.
+      ( for more details, see
+        response_time_le_WCRT: .
+        completed_by_end_time: model/schedule/uni/end_time.v
+        completes_at_end_time: model/schedule/uni/end_time.v
+      ) *)
+    Theorem uniprocessor_response_time_bound_TDMA: response_time_bounded_by tsk BOUND.
+    Proof.
+      intros j arr_seq_j JobTsk.
+      apply completion_monotonic with (t:=job_arrival j + RT j);first exact.
+      - rewrite leq_add2l /BOUND. 
+        apply (response_time_le_WCRT) 
+        with (task_cost0:=task_cost) (task_deadline0:=task_deadline)(sched0:=sched)
+             (job_arrival0:=job_arrival)(job_cost0:=job_cost)(job_deadline0:=job_deadline)
+             (job_task0:=job_task)(ts0:=ts)(arr_seq0:=arr_seq)
+             (slot_order0:=slot_order)(Job0:=Job)(tsk0:=tsk); try done;auto;try (intros; 
+        by apply all_previous_jobs_of_same_task_completed).
+      - apply completed_by_end_time 
+        with (sched0:=sched)(job_arrival0:=job_arrival)
+             (job_cost0:=job_cost); first exact.
+        apply completes_at_end_time
+        with 
+             (job_arrival0:=job_arrival)(task_cost0:=task_cost)(arr_seq0:=arr_seq)
+             (job_task0:=job_task)(job_deadline0:=job_deadline)(task_deadline0:=task_deadline)
+             (sched0:=sched)(ts0:=ts)(slot_order0:=slot_order)
+             (tsk0:=tsk) (j0:=j); try auto;try (intros; 
+        by apply all_previous_jobs_of_same_task_completed).
+    Qed. 
+
+    (** Sufficient Analysis *)
+    (* Finally, we show that the RTA is a sufficient schedulability analysis. *)
+    Section AnalysisIsSufficient.
+
+      (* Assume that BOUND is a valid tdma bound *)
+      Hypothesis H_is_valid_bound:
+        is_valid_tdma_bound BOUND.
+
+      (* We can prove the theorem: there is no deadline miss of task tsk *)
+      Theorem taskset_schedulable_by_tdma : no_deadline_missed_by_task tsk.
+      Proof.
+        apply task_completes_before_deadline with (task_deadline0:=task_deadline) (R:=BOUND)
+        ;try done.
+        move => j arr_seqJ.
+        - by apply H_valid_job_parameters.
+        - apply uniprocessor_response_time_bound_TDMA.
+      Qed.
+
+      (* Based on the theorem above, we can prove that
+         any job of the arrival sequence are spawned by task tsk won't miss its deadline. *)
+      Theorem jobs_schedulable_by_tdma_rta :
+        forall j,
+          arrives_in arr_seq j /\ job_task j =tsk -> 
+          no_deadline_missed_by_job j.
+      Proof.
+        intros j [arr_seqJ Jtsk].
+        by apply taskset_schedulable_by_tdma.
+      Qed.
+
+    End AnalysisIsSufficient.
+
+  End ResponseTimeBound.
+
+End ResponseTimeAnalysisTDMA.
+
+
+

implementation/uni/basic/extraction_tdma.v

+(* Require Import Extraction. *) (* Required for Coq 8.7 *)
+Require Import rt.analysis.uni.basic.tdma_wcrt_analysis.
+From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq bigop div.
+
+Set Implicit Arguments.
+
+CoInductive Task_T :Type:=
+  build_task: nat->nat->nat->nat -> 
+              Task_T.
+
+Definition get_slot(tsk:Task_T):= 
+  match tsk with
+  | build_task x  _ _ _  => x end.
+
+Definition get_cost (tsk:Task_T):=
+ match tsk with
+  | build_task _ x _ _  => x end.
+
+Definition get_D (tsk:Task_T):=
+ match tsk with
+  | build_task _ _ x _  => x end.
+
+Definition get_P (tsk:Task_T):=
+  match tsk with
+  | build_task _ _ _ x => x end.
+
+Definition task_eq (t1 t2: Task_T) :=
+      (get_slot t1 == get_slot t2)&&
+      (get_cost t1 == get_cost t2)&&
+      (get_D t1 == get_D t2)&&
+      (get_P t1 == get_P t2) .
+
+Fixpoint In (a:Task_T) (l:list Task_T) : Prop :=
+    match l with
+      | nil => False
+      | b :: m =>  a=b \/ In a m
+    end.
+
+Definition schedulable_tsk T tsk:=
+    let bound := WCRT_OneJobTDMA.WCRT_formula T (get_slot tsk) (get_cost tsk) in
+  if (bound <= get_D tsk)&& (bound <= get_P tsk) then true else false .
+
+Fixpoint schedulability_test T (l: list Task_T):=
+match l with
+|nil => true
+|x::s=> (schedulable_tsk T x) && (schedulability_test T s)
+end.
+
+Theorem schedulability_test_valid T TL:
+schedulability_test T TL
+    <-> (forall tsk, In tsk TL ->schedulable_tsk T tsk) .
+Proof.
+induction TL;split;auto.
+- intros STL tsk IN. rewrite /= in IN. move:IN=> [EQ |IN];
+  rewrite /= in STL; move/andP in STL.
+  + rewrite EQ;apply STL.
+  + apply IHTL. apply STL. assumption.
+- intro ALL. apply/andP;split.
+  + apply ALL. simpl;by left.
+  + apply IHTL;intros tsk IN;apply ALL;simpl;by right.
+Qed. 
+
+Definition cycle l:=
+(foldr plus 0 (map get_slot l)).
+
+Definition schedulability_tdma (l: list Task_T):=
+schedulability_test (cycle l) l.
+
+Theorem schedulability_tdma_valid task_list:
+   schedulability_tdma task_list
+    <-> (forall tsk, In tsk task_list ->schedulable_tsk (cycle task_list) tsk) .
+Proof.
+rewrite /schedulability_tdma. apply schedulability_test_valid.
+Qed.
+
+(*Eval compute in cycle [:: build_task(2,3,4,4);(6,2,5,6)].
+
+Eval compute in WCRT_OneJobTDMA.WCRT_formula 4 2 3.
+
+Eval compute in schedulability_tdma [::(2,3,7,7);(1,2,6,6)]. *)
+
+(*Extract Inductive unit => "unit" [ "()" ].
+Extract Inductive bool =>"bool" [ "true" "false" ].
+Extract Inductive nat => int [ "0" "Pervasives.succ" ]
+ "(fun fO fS n -> if n=0 then fO () else fS (n-1))".
+Extract Inductive list => "list" [ "[]" "(::)" ].
+Extract Constant eqn => "(=)".
+Extract Constant addn => "(+)".
+Extract Constant subn => "fun n m -> Pervasives.max 0 (n-m)".
+Extract Constant muln => "( * )".
+Extract Inlined Constant leq => "(<=)".
+Recursive Extraction schedulability_tdma.
+Extraction "schedulability_tdma.ml" schedulability_tdma. *)
\ No newline at end of file

implementation/uni/basic/schedule_tdma.v

+Require Import rt.util.all rt.util.find_seq
+               Arith.
+Require Import rt.model.arrival.basic.job
+               rt.model.arrival.basic.arrival_sequence
+               rt.model.schedule.uni.basic.platform_tdma
+               rt.model.arrival.basic.task rt.model.policy_tdma.
+Require Import rt.model.schedule.uni.schedule rt.model.schedule.uni.schedulability.
+Require Import rt.model.priority
+               rt.analysis.uni.basic.tdma_rta_theory
+               rt.model.schedule.uni.transformation.construction.
+Require Import rt.implementation.job rt.implementation.task
+               rt.implementation.arrival_sequence
+               rt.implementation.uni.basic.schedule.
+
+From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq bigop div.
+
+Set Bullet Behavior "Strict Subproofs".
+Module ConcreteSchedulerTDMA.
+
+  Import Job ArrivalSequence UniprocessorSchedule SporadicTaskset Schedulability Priority
+         ResponseTimeAnalysisTDMA PolicyTDMA ScheduleConstruction Platform_TDMA.
+  Import ConcreteJob ConcreteTask ConcreteArrivalSequence ConcreteScheduler BigOp.
+ 
+  Section ImplementationTDMA.
+
+    Context {Task: eqType}.
+    Context {Job: eqType}.
+    Variable job_arrival: Job -> time.
+    Variable job_cost: Job -> time.
+    Variable job_task: Job -> Task.
+
+    Variable arr_seq: arrival_sequence Job.
+
+    Variable ts: {set Task}.
+
+    Variable time_slot: TDMA_slot Task.
+
+    Variable slot_order: TDMA_slot_order Task.
+
+    Hypothesis H_arrival_times_are_consistent: 
+        arrival_times_are_consistent job_arrival arr_seq.
+
+    Section JobSchedule.
+
+        Variable sched: schedule Job.
+        Variable t:time.
+
+        Let is_pending := pending job_arrival job_cost sched.
+
+        Definition pending_jobs:=
+             [seq j <- jobs_arrived_up_to arr_seq t | is_pending j t].
+
+
+        Let job_in_time_slot:=
+          fun job => Task_in_time_slot ts slot_order (job_task job) time_slot t.
+
+
+        Definition job_to_schedule :=
+          findP job_in_time_slot pending_jobs.
+
+      Section Lemmas.
+
+        Hypothesis arr_seq_is_a_set:
+          arrival_sequence_is_a_set arr_seq.
+
+        Lemma pending_jobs_uniq:
+          uniq pending_jobs.
+        Proof.
+        apply filter_uniq
+        , arrivals_uniq with (job_arrival0:=job_arrival);auto.
+        Qed.
+
+
+        Lemma respects_FIFO:
+          forall j j', j \in pending_jobs -> j' \in pending_jobs ->
+          find (fun job => job==j') pending_jobs
+           < find (fun job => job==j) pending_jobs ->
+          job_arrival j' <= job_arrival j.
+        Proof.
+        rewrite /job_to_schedule /pending_jobs /jobs_arrived_up_to
+        /jobs_arrived_between. intros*.
+        repeat rewrite mem_filter.
+        move=> /andP [PENJ JIN] /andP [PENJ' J'IN] LEQ.
+        apply mem_bigcat_nat_exists in JIN.
+        apply mem_bigcat_nat_exists in J'IN.
+        destruct JIN as [arrj [JIN _]].
+        destruct J'IN as [arrj' [J'IN _]].
+        have ARRJ: job_arrival j = arrj by eauto.
+        have ARRJ': job_arrival j' = arrj' by eauto.
+        have JLT: arrj' <= t by move:PENJ'=>/andP [HAD _]; eauto.
+        destruct (leqP arrj' arrj) as [G|G]. eauto.
+        apply mem_bigcat_nat with (m:=0) (n:=arrj.+1) in JIN;auto.
+        apply mem_bigcat_nat with (m:=arrj.+1) (n:=t.+1) in J'IN;auto.
+        have BIGJ: j \in [seq j <- \big[cat/[::]]_(0 <= i < arrj.+1)
+                    jobs_arriving_at arr_seq i | is_pending j t]
+        by rewrite mem_filter;apply /andP.
+        have BIGJ': j' \in [seq j <- \big[cat/[::]]_(arrj.+1 <= i < t.+1)
+                    jobs_arriving_at arr_seq i | is_pending j t]
+        by rewrite mem_filter;apply /andP.
+        rewrite ->big_cat_nat with (n:=arrj.+1) in LEQ;try ssromega.
+        rewrite filter_cat find_cat /=in LEQ.
+        rewrite find_cat /= in LEQ.
+        have F: (has (fun job : Job => job == j')
+          [seq j <- \big[cat/[::]]_(0 <= i < arrj.+1)
+                       jobs_arriving_at arr_seq i
+             | is_pending j t]) = false .
+        apply find_uniq with (l2:=
+        [seq j <- \big[cat/[::]]_(arrj.+1 <= i < t.+1)
+                       jobs_arriving_at arr_seq i
+             | is_pending j t]);auto.
+        rewrite -filter_cat -big_cat_nat;auto. apply pending_jobs_uniq.
+        ssromega.
+        have TT: (has (fun job : Job => job == j)
+          [seq j <- \big[cat/[::]]_(0 <= i < arrj.+1)
+                       jobs_arriving_at arr_seq i
+             | is_pending j t]) = true. apply /hasP. by exists j.
+        have FI: find (fun job : Job => job == j)
+          [seq j <- \big[cat/[::]]_(0 <= t < arrj.+1)
+                       jobs_arriving_at arr_seq t
+             | is_pending j t] < size (
+          [seq j <- \big[cat/[::]]_(0 <= t < arrj.+1)
+                       jobs_arriving_at arr_seq t
+             | is_pending j t]). by rewrite -has_find.
+       rewrite F TT in LEQ. ssromega.
+        Qed.
+      
+        Lemma pending_job_in_penging_list:
+          forall j, arrives_in arr_seq j ->
+          pending job_arrival job_cost sched j t ->
+          j \in pending_jobs.
+        Proof.
+        intros* ARRJ PEN.
+        rewrite mem_filter. apply /andP. split.
+        apply PEN. rewrite /jobs_arrived_up_to.
+        apply arrived_between_implies_in_arrivals with (job_arrival0:=job_arrival).
+        apply H_arrival_times_are_consistent. auto.
+        rewrite /arrived_between. simpl. 
+        rewrite /pending in PEN. move:PEN=>/andP [ARRED _].
+        rewrite /has_arrived in ARRED. auto.
+        Qed.
+
+        Lemma pendinglist_jobs_in_arr_seq:
+          forall j, j \in pending_jobs ->
+           arrives_in arr_seq j.
+        Proof.
+        intros* JIN.
+        rewrite mem_filter in JIN. move /andP in JIN.
+        destruct JIN as [PEN ARR]. rewrite /jobs_arrived_up_to in ARR.
+        by apply in_arrivals_implies_arrived with (t1:= 0)(t2:= t.+1).
+        Qed.
+      End Lemmas.
+
+    End JobSchedule.
+
+
+
+    Section SchedulerTDMA.
+
+        Let empty_schedule : schedule Job := fun t => None.
+        Definition scheduler_tdma:=
+           build_schedule_from_prefixes job_to_schedule empty_schedule.
+
+        Lemma scheduler_depends_only_on_prefix:
+          forall sched1 sched2 t,
+          (forall t0, t0 < t -> sched1 t0 = sched2 t0) ->
+          job_to_schedule sched1 t = job_to_schedule sched2 t.
+        Proof.
+        intros * ALL.
+        rewrite /job_to_schedule. f_equal.
+        apply eq_in_filter.
+        intros j ARR.
+        apply in_arrivals_implies_arrived_before 
+        with (job_arrival0 := job_arrival) in ARR.
+        rewrite /arrived_before ltnS in ARR.
+        rewrite /pending /has_arrived ARR. repeat rewrite andTb; f_equal.
+        rewrite /completed_by; f_equal.
+        apply eq_big_nat. intros.
+        by rewrite /service_at /scheduled_at ALL.
+        assumption.
+      Qed.
+
+      Lemma scheduler_uses_construction_function:
+      forall t, scheduler_tdma t = job_to_schedule scheduler_tdma t.
+      Proof.
+      intro t. apply prefix_dependent_schedule_construction.
+      apply scheduler_depends_only_on_prefix.
+      Qed.
+
+    End SchedulerTDMA.
+
+    
+    Let sched:=
+      scheduler_tdma.
+
+
+    Theorem scheduler_jobs_must_arrive_to_execute:
+      jobs_must_arrive_to_execute job_arrival sched.
+    Proof.
+      move => j t /eqP SCHED.
+      rewrite /sched scheduler_uses_construction_function /job_to_schedule in SCHED.
+      apply findP_in_seq in SCHED. move:SCHED => [IN PEN].
+      rewrite mem_filter in PEN.
+      by move: PEN => /andP [/andP [ARR _] _].
+    Qed.
+
+    Theorem scheduler_completed_jobs_dont_execute:
+      completed_jobs_dont_execute job_cost sched.
+    Proof.
+      intros j t.
+      induction t;
+        first by rewrite /service /service_during big_geq //.
+      rewrite /service /service_during big_nat_recr //=.
+      rewrite leq_eqVlt in IHt; move: IHt => /orP [/eqP EQ | LT]; last first.
+      {
+        apply: leq_trans LT; rewrite -addn1.
+          by apply leq_add; last by apply leq_b1.
+      }
+      rewrite -[job_cost _]addn0; apply leq_add; first by rewrite -EQ.
+      rewrite leqn0 eqb0 /scheduled_at.
+      rewrite /sched scheduler_uses_construction_function //.
+      rewrite /job_to_schedule.
+      apply/eqP; intro FIND.
+      apply findP_in_seq in FIND. move:FIND => [IN PEN].
+      by rewrite mem_filter /pending /completed_by -EQ eq_refl andbF andFb in PEN.
+    Qed.
+
+  End ImplementationTDMA.
+
+End ConcreteSchedulerTDMA.
\ No newline at end of file

implementation/uni/basic/tdma_rta_example.v

+Require Import rt.util.all rt.util.find_seq
+               .
+Require Import rt.model.arrival.basic.job
+               rt.model.arrival.basic.arrival_sequence
+               rt.model.schedule.uni.basic.platform_tdma
+               rt.model.arrival.basic.task rt.model.policy_tdma.
+Require Import rt.model.schedule.uni.schedule rt.model.schedule.uni.schedulability.
+Require Import rt.model.priority
+               rt.analysis.uni.basic.tdma_rta_theory
+               rt.analysis.uni.basic.tdma_wcrt_analysis.
+Require Import rt.implementation.job rt.implementation.task
+               rt.implementation.arrival_sequence
+               rt.implementation.uni.basic.schedule_tdma.
+
+From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq bigop div.
+
+Set Bullet Behavior "Strict Subproofs".
+Module ResponseTimeAnalysisExemple.
+
+  Import Job ArrivalSequence UniprocessorSchedule SporadicTaskset Schedulability Priority
+         ResponseTimeAnalysisTDMA PolicyTDMA  Platform_TDMA.
+  Import ConcreteJob ConcreteTask ConcreteArrivalSequence  BigOp
+         ConcreteSchedulerTDMA WCRT_OneJobTDMA.
+ 
+
+  Section ExampleTDMA.
+
+    Context {Job: eqType}.
+
+    Let tsk1 := {| task_id := 1; task_cost := 1; task_period := 16; task_deadline := 15|}.
+    Let tsk2 := {| task_id := 2; task_cost := 1; task_period := 8; task_deadline := 5|}.
+    Let tsk3 := {| task_id := 3; task_cost := 1; task_period := 9; task_deadline := 6|}.
+
+
+
+    Let time_slot1 := 1.
+    Let time_slot2 := 4.
+    Let time_slot3 := 3.
+
+    Program Let ts := Build_set [:: tsk1; tsk2; tsk3] _.
+
+    Let slot_seq := [::(tsk1,time_slot1);(tsk2,time_slot2);(tsk3,time_slot3)].
+
+    Fact ts_has_valid_parameters:
+      valid_sporadic_taskset task_cost task_period task_deadline ts.
+    Proof.
+      intros tsk tskIN.
+      repeat (move: tskIN => /orP [/eqP EQ | tskIN]; subst; compute); by done.
+    Qed.
+
+    Let arr_seq := periodic_arrival_sequence ts.
+
+    Fact job_arrival_times_are_consistent:
+      arrival_times_are_consistent job_arrival arr_seq.
+    Proof.
+    apply periodic_arrivals_are_consistent.
+    Qed.
+
+
+    Definition time_slot task:=
+      if task \in (map fst slot_seq) then 
+      let  n:= find (fun tsk => tsk==task)(map fst slot_seq) in
+       nth n (map snd slot_seq) n else 0. 
+
+
+    Fact valid_time_slots:
+      forall tsk, tsk \in ts ->
+        is_valid_time_slot tsk time_slot.
+    Proof.
+    apply/allP. by cbn.
+    Qed.
+
+    Definition slot_order task1 task2:=
+      task_id task1 >= task_id task2.
+
+
+    Let sched:=
+      scheduler_tdma job_arrival job_cost job_task arr_seq ts time_slot slot_order.
+
+    Let job_in_time_slot t j:=
+      Task_in_time_slot ts slot_order (job_task j) time_slot t.
+
+    Fact slot_order_total:
+      slot_order_is_total_over_task_set ts slot_order.
+    Proof.
+    intros t1 t2 IN1 IN2. rewrite /slot_order.
+    case LEQ: (_ <= _);first by left. 
+    right;move/negP /negP in LEQ;rewrite -ltnNge in LEQ;auto.
+    Qed.
+
+    Fact slot_order_transitive:
+      slot_order_is_transitive slot_order.
+    Proof.
+    rewrite /slot_order.
+    intros t1 t2 t3 IN1 IN2. ssromega.
+    Qed.
+
+    Fact slot_order_antisymmetric:
+      slot_order_is_antisymmetric_over_task_set ts slot_order.
+    Proof.
+    intros x y IN1 IN2. rewrite /slot_order. intros O1 O2.
+    have EQ: task_id x = task_id y by ssromega.
+    case (x==y)eqn:XY;move/eqP in XY;auto.
+    repeat (move:IN2=> /orP [/eqP TSK2 |IN2]); repeat (move:IN1=>/orP [/eqP TSK1|IN1];subst);compute ;try done.
+    Qed.
+
+    Fact respects_TDMA_policy:
+      Respects_TDMA_policy job_arrival job_cost job_task arr_seq sched ts time_slot slot_order.
+    Proof.
+    intros j t ARRJ.
+    split.
+    - rewrite /sched_implies_in_slot /scheduled_at /sched scheduler_uses_construction_function /job_to_schedule.
+      move => /eqP FUN. unfold job_in_time_slot.
+      apply findP_in_seq in FUN.
+      by destruct FUN as [ TskInSlot _].
+      apply job_arrival_times_are_consistent.
+    - rewrite /backlogged_implies_not_in_slot_or_other_job_sched /backlogged /scheduled_at /sched scheduler_uses_construction_function /job_to_schedule.
+      move => /andP [PEN NOSCHED]. have NSJ:= NOSCHED.
+      apply findP_notSome_in_seq in NOSCHED.
+      destruct NOSCHED as [NOIN |EXIST].
+      + by left.
+      + case (Task_in_time_slot ts slot_order (job_task j) time_slot t) eqn:INSLOT;last by left.
+        right. destruct EXIST as [y SOMEY]. exists y. have FIND:=SOMEY. apply findP_in_seq in SOMEY.
+        move:SOMEY => [SLOTY YIN]. have ARRY: arrives_in arr_seq y
+        by apply pendinglist_jobs_in_arr_seq in YIN.
+        have SAMETSK: job_task j = job_task y.
+        have EQ:Task_in_time_slot ts slot_order (job_task y) time_slot t =
+                  Task_in_time_slot ts slot_order (job_task j) time_slot t by rewrite INSLOT. 
+        apply task_in_time_slot_uniq with (ts0:= ts) (t0:=t) (slot_order:=slot_order) (task_time_slot:=time_slot);auto.
+        intros;by apply slot_order_total.
+        by apply slot_order_antisymmetric.
+        by apply slot_order_transitive.
+        by apply periodic_arrivals_all_jobs_from_taskset.
+        by apply valid_time_slots,periodic_arrivals_all_jobs_from_taskset.
+        by apply periodic_arrivals_all_jobs_from_taskset.
+        by apply valid_time_slots ,periodic_arrivals_all_jobs_from_taskset.
+        split;auto.
+        * split;case (y==j)eqn:YJ;move/eqP in YJ;try by rewrite FIND YJ in NSJ;move/eqP in NSJ;auto.
+          apply pending_job_in_penging_list with (arr_seq0:=arr_seq) in PEN;auto
+          ;last apply job_arrival_times_are_consistent.
+          apply findP_FIFO with (y0:=j) in FIND;auto. fold sched in FIND.
+          apply (respects_FIFO ) in FIND;auto.
+          apply periodic_arrivals_are_sporadic with (ts:=ts) in FIND;auto.
+          have PERIODY:task_period (job_task y)>0 by
+          apply ts_has_valid_parameters,periodic_arrivals_all_jobs_from_taskset. ssromega.  
+          apply  job_arrival_times_are_consistent.
+          apply periodic_arrivals_is_a_set,ts_has_valid_parameters.
+          split;auto.
+          by apply/eqP.
+      + apply pending_job_in_penging_list;trivial.
+        * by apply job_arrival_times_are_consistent.
+      + by apply job_arrival_times_are_consistent.
+    Qed.
+
+
+    Fact job_cost_le_task_cost:
+      forall j : concrete_job_eqType,
+      arrives_in arr_seq j ->
+      job_cost_le_task_cost task_cost job_cost job_task j.
+    Proof.
+    intros JOB ARR.
+    apply periodic_arrivals_valid_job_parameters in ARR.
+    apply ARR. by apply ts_has_valid_parameters.
+    Qed.
+
+
+    Let tdma_claimed_bound task:= 
+      WCRT task_cost time_slot ts task.
+    Let tdma_valid_bound task := is_valid_tdma_bound task_deadline task (tdma_claimed_bound task).
+
+    Fact valid_tdma_bounds:
+      forall tsk, tsk \in ts ->
+        tdma_valid_bound tsk = true.
+    Proof.
+    apply/allP.
+    rewrite /tdma_valid_bound /tdma_claimed_bound /WCRT /TDMA_cycle.
+    rewrite bigopE. by compute.
+    Qed.
+
+    Fact WCRT_le_period:
+      forall tsk, tsk \in ts ->
+      WCRT task_cost time_slot ts tsk <= task_period tsk.
+    Proof.
+    apply/allP.
+    rewrite /tdma_valid_bound /tdma_claimed_bound /WCRT /TDMA_cycle.
+    rewrite bigopE. by compute.
+    Qed.
+
+
+    Let no_deadline_missed_by :=
+      task_misses_no_deadline job_arrival job_cost job_deadline job_task arr_seq sched.
+
+    Theorem ts_is_schedulable_by_tdma :
+      forall tsk, tsk \in ts ->
+        no_deadline_missed_by tsk.
+    Proof.
+    intros tsk tskIN.
+    have VALID_JOB := periodic_arrivals_valid_job_parameters ts ts_has_valid_parameters.
+    apply taskset_schedulable_by_tdma with (task_deadline:=task_deadline)(task_period:=task_period) 
+    (tsk0:=tsk)(ts0:=ts)(task_cost:=task_cost)
+    (task_time_slot:=time_slot) (slot_order:= slot_order)
+    (arr_seq0:=arr_seq).
+    - apply job_arrival_times_are_consistent.
+    - apply periodic_arrivals_are_sporadic.
+    - apply scheduler_jobs_must_arrive_to_execute.
+      apply job_arrival_times_are_consistent.
+    - apply scheduler_completed_jobs_dont_execute.
+      apply job_arrival_times_are_consistent.
+    - assumption.
+    - by apply WCRT_le_period.
+    - by apply respects_TDMA_policy.
+    - by apply valid_time_slots.
+    - assumption.
+    - by apply job_cost_le_task_cost.
+    - apply valid_tdma_bounds;auto.
+    Qed.
+
+  End ExampleTDMA.
+
+End ResponseTimeAnalysisExemple.
+
+
+
+

model/policy_tdma.v

+Require Import  rt.util.all.
+Require Import  rt.model.time
+                rt.model.arrival.basic.task 
+                rt.model.arrival.basic.job.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop div.
+
+Module PolicyTDMA.
+
+  Import Time.
+
+  (** In this section, we define the TDMA policy.*)
+  Section TDMA.
+    (* The TDMA policy is based on two properties.
+      (1) Each task has a fixed, reserved time slot for execution;
+      (2) These time slots are ordered in sequence to form a TDMA cycle, which repeats along the timeline.
+      An example of TDMA schedule is illustrated in the following.
+      ______________________________
+      | s1 |  s2  |s3| s1 |  s2  |s3|...
+      --------------------------------------------->
+      0                                            t
+    *)
+    Variable Task: eqType.
+    (* With each task, we associate the duration of the corresponding TDMA slot. *)
+    Definition TDMA_slot:= Task -> duration.
+    (* Moreover, within each TDMA cycle, task slots are ordered according to some relation. *)
+    Definition TDMA_slot_order:= rel Task.
+
+  End TDMA.
+
+  (** In this section, we define the properties of TDMA and prove some basic lemmas. *)
+  Section PropertiesTDMA.
+
+    Context {Task:eqType}.
+
+    (* Consider any task set ts... *)
+    Variable ts: {set Task}.
+
+    (* ...and any slot order (i.e, slot_order slot1 slot2 means that slot1 comes before slot2 in a TDMA cycle). *)
+    Variable slot_order: TDMA_slot_order Task.
+
+    (* First, we define the properties of a valid time slot order. *)
+    Section Relation.
+      (* Time slot order must transitive... *)
+      Definition slot_order_is_transitive:= transitive slot_order.
+
+      (* ..., totally ordered over the task set... *)
+      Definition slot_order_is_total_over_task_set :=
+        total_over_list slot_order ts.
+
+      (* ... and antisymmetric over task set. *)
+      Definition slot_order_is_antisymmetric_over_task_set :=
+        antisymmetric_over_list slot_order ts. 
+
+    End Relation.
+
+    (* Next, we define some properties of task time slots *)
+    Section TimeSlot.
+
+      (* Consider any task in task set ts*)
+      Variable task: Task.
+      Hypothesis H_task_in_ts: task \in ts. 
+
+      (* Consider any TDMA slot assignment for these tasks *)
+      Variable task_time_slot: TDMA_slot Task.
+
+      (* A valid time slot must be positive *)
+      Definition is_valid_time_slot:=
+        task_time_slot task > 0.
+
+      (* We define the TDMA cycle as the sum of all the tasks' time slots *)
+      Definition TDMA_cycle:= 
+        \sum_(tsk <- ts) task_time_slot tsk.
+
+       (* We define the function returning the slot offset for each task: 
+         i.e., the distance between the start of the TDMA cycle and 
+         the start of the task time slot *)
+      Definition Task_slot_offset:= 
+        \sum_(prev_task <- ts | slot_order prev_task task && (prev_task != task)) task_time_slot prev_task.
+
+      (* The following function tests whether a task is in its time slot at instant t *)
+      Definition Task_in_time_slot (t:time):=
+       ((t + TDMA_cycle - (Task_slot_offset)%% TDMA_cycle) %% TDMA_cycle) 
+        < (task_time_slot task).
+
+      Section BasicLemmas.
+
+        (* Assume task_time_slot is valid time slot*)
+        Hypothesis time_slot_positive:
+          is_valid_time_slot.
+
+        (* Obviously, the TDMA cycle is greater or equal than any task time slot which is 
+          in TDMA cycle *)
+        Lemma TDMA_cycle_ge_each_time_slot:
+          TDMA_cycle >= task_time_slot task.
+        Proof. 
+        rewrite /TDMA_cycle (big_rem task) //.
+        apply:leq_trans; last by exact: leq_addr.
+        by apply leqnn.
+        Qed.
+
+        (* Thus, a TDMA cycle is always positive *)
+        Lemma TDMA_cycle_positive:
+          TDMA_cycle > 0.
+        Proof.
+        move:time_slot_positive. move/leq_trans;apply;apply TDMA_cycle_ge_each_time_slot.
+        Qed.
+
+        (* Slot offset is less then cycle *)
+        Lemma Offset_lt_cycle:
+          Task_slot_offset < TDMA_cycle.
+        Proof.
+        rewrite /Task_slot_offset /TDMA_cycle big_mkcond.
+        apply leq_ltn_trans with (n:=\sum_(prev_task <- ts )if prev_task!=task then task_time_slot prev_task else 0).
+        - apply leq_sum. intros* T. case (slot_order i task);auto.
+        - rewrite -big_mkcond. rewrite-> bigD1_seq with (j:=task);auto.
+          rewrite -subn_gt0 -addnBA. rewrite subnn addn0 //.
+          trivial. apply (set_uniq ts).
+        Qed.
+
+        (* For a task, the sum of its slot offset and its time slot is 
+          less then or equal to cycle. *)
+        Lemma Offset_add_slot_leq_cycle:
+          Task_slot_offset + task_time_slot task <= TDMA_cycle.
+        Proof.
+        rewrite /Task_slot_offset /TDMA_cycle.
+        rewrite addnC (bigD1_seq task) //=. rewrite leq_add2l.
+        rewrite big_mkcond.
+        replace (\sum_(i <- ts | i != task) task_time_slot i)
+        with (\sum_(i <- ts ) if i != task then task_time_slot i else 0).
+        apply leq_sum. intros*T. case (slot_order i task);auto.
+        by rewrite -big_mkcond. apply (set_uniq ts).
+        Qed.
+
+      End BasicLemmas.
+
+    End TimeSlot.
+
+    (* In this section, we prove that no two tasks share the same time slot at any time. *)
+    Section InTimeSlotUniq.
+
+      (* Consider any TDMA slot assignment for these tasks *)
+      Variable task_time_slot: TDMA_slot Task.
+
+      (* Assume that slot order is total... *)
+      Hypothesis slot_order_total:
+        slot_order_is_total_over_task_set.
+
+      (*..., antisymmetric... *)
+      Hypothesis slot_order_antisymmetric:
+        slot_order_is_antisymmetric_over_task_set.
+
+      (*... and transitive. *)
+      Hypothesis slot_order_transitive:
+        slot_order_is_transitive.
+
+      (* Then, we can prove that the difference value between two offsets is
+        at least a slot *)
+      Lemma relation_offset:
+        forall tsk1 tsk2, tsk1 \in ts -> tsk2 \in ts ->
+        slot_order tsk1 tsk2 -> tsk1 != tsk2 ->
+        Task_slot_offset tsk2 task_time_slot >= Task_slot_offset tsk1 task_time_slot + task_time_slot tsk1 .
+      Proof.
+      intros* IN1 IN2 ORDER NEQ.
+      rewrite /Task_slot_offset big_mkcond addnC.
+      replace (\sum_(tsk <- ts | slot_order tsk tsk2 && (tsk != tsk2)) task_time_slot tsk)
+        with (task_time_slot tsk1 + \sum_(tsk <- ts )if slot_order tsk tsk2 && (tsk != tsk1) && (tsk!=tsk2) then task_time_slot tsk else O).
+      rewrite leq_add2l. apply leq_sum_seq. intros* IN T.
+      case (slot_order i tsk1)eqn:SI2;auto. case (i==tsk1)eqn:IT2;auto;simpl.
+      case (i==tsk2)eqn:IT1;simpl;auto.
+      - by move/eqP in IT1;rewrite IT1 in SI2;apply slot_order_antisymmetric in ORDER;auto;apply ORDER in SI2;move/eqP in NEQ.
+      - by rewrite (slot_order_transitive _ _ _ SI2 ORDER).
+      - symmetry. rewrite big_mkcond /=. rewrite->bigD1_seq with (j:=tsk1);auto;last by apply (set_uniq ts).
+        move/eqP /eqP in ORDER. move/eqP in NEQ. rewrite ORDER //=. apply /eqP.
+        have TS2: (tsk1 != tsk2) = true . apply /eqP;auto. rewrite TS2.
+        rewrite eqn_add2l. rewrite big_mkcond. apply/eqP. apply eq_bigr;auto.
+        intros* T. case(i!=tsk1);case (slot_order i tsk2);case (i!=tsk2) ;auto.
+      Qed.
+
+      (* Then, we proved that no two tasks share the same time slot at any time. *)
+      Lemma task_in_time_slot_uniq:
+        forall tsk1 tsk2 t, tsk1 \in ts -> task_time_slot tsk1 > 0 ->
+        tsk2 \in ts -> task_time_slot tsk2 > 0 ->
+        Task_in_time_slot tsk1 task_time_slot t ->
+        Task_in_time_slot tsk2 task_time_slot t ->
+        tsk1 = tsk2.
+      Proof.
+      intros* IN1 SLOT1 IN2 SLOT2.
+      rewrite /Task_in_time_slot.
+      set cycle:=TDMA_cycle task_time_slot.
+      set O1:= Task_slot_offset tsk1 task_time_slot.
+      set O2:= Task_slot_offset tsk2 task_time_slot.
+      have CO1: O1 < cycle by apply Offset_lt_cycle.
+      have CO2: O2 < cycle by apply Offset_lt_cycle.
+      have C: cycle > 0 by apply (TDMA_cycle_positive tsk1).
+      have GO1:O1 %% cycle = O1 by apply modn_small,Offset_lt_cycle. rewrite GO1.
+      have GO2:O2 %% cycle = O2 by apply modn_small,Offset_lt_cycle. rewrite GO2.
+      have SO1:O1 + task_time_slot tsk1 <= cycle by apply (Offset_add_slot_leq_cycle tsk1).
+      have SO2:O2 + task_time_slot tsk2 <= cycle by apply (Offset_add_slot_leq_cycle tsk2).
+      repeat rewrite mod_elim;auto.
+      case (O1 <= t%%cycle)eqn:O1T;case (O2 <= t %%cycle)eqn:O2T;intros G1 G2;try ssromega.
+      apply ltn_subLR in G1;apply ltn_subLR in G2. case (tsk1==tsk2) eqn:NEQ;move/eqP in NEQ;auto.
+      destruct (slot_order_total tsk1 tsk2) as [order |order];auto;apply relation_offset in order;
+      fold O1 O2 in order;try ssromega;auto. by move/eqP in NEQ. apply /eqP;auto.
+      Qed.
+
+    End InTimeSlotUniq.
+
+  End PropertiesTDMA.
+
+End PolicyTDMA.
+
+
+

model/schedule/uni/basic/platform_tdma.v

+Require Import  rt.util.all.
+Require Import  rt.model.arrival.basic.task 
+                rt.model.arrival.basic.job rt.model.priority 
+                rt.model.arrival.basic.task_arrival
+                rt.model.schedule.uni.schedule.
+Require Import  rt.model.policy_tdma.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
+
+Module Platform_TDMA.
+
+  Import Job  UniprocessorSchedule div.
+  Export PolicyTDMA.
+
+  (* In this section, we define properties of the processor platform for TDMA. *)
+  Section Properties.
+    
+    Context {sporadic_task: eqType}.
+    Context {Job: eqType}.
+    Variable job_arrival: Job -> time.
+    Variable job_cost: Job -> time.
+    Variable job_deadline: Job -> time.
+    Variable job_task: Job -> sporadic_task.
+
+    (* Consider any job arrival sequence... *)
+    Variable arr_seq: arrival_sequence Job.
+
+    (* ..., any uniprocessor... *)
+    Variable sched: schedule Job.
+
+    (* ... and any sporadic task set. *)
+    Variable ts: {set sporadic_task}.
+
+    (* Consider any TDMA slot assignment... *)
+    Variable time_slot: TDMA_slot sporadic_task.
+
+    (* ... and any slot order. *)
+    Variable slot_order: TDMA_slot_order sporadic_task.
+
+    (* In order to characterize a TDMA policy, we first define whether a job is executing its TDMA slot at time t. *)
+    Let job_in_time_slot (job:Job) (t:instant):= 
+        Task_in_time_slot ts slot_order (job_task job) time_slot t. 
+     
+    (* We say that a TDMA policy is respected by the schedule iff 
+       1. when a job is scheduled at time t, then the corresponding task 
+          is also in its own time slot... *)
+    Definition sched_implies_in_slot j t:=
+      (scheduled_at sched j t -> job_in_time_slot j t).
+
+    (* 2. when a job is backlogged at time t,the corresponding task 
+          isn't in its own time slot or another previous job of the same task is scheduled *)
+    Definition backlogged_implies_not_in_slot_or_other_job_sched j t:=
+      (backlogged job_arrival job_cost sched j t -> 
+        ~ job_in_time_slot j t \/ 
+        (exists j_other, arrives_in arr_seq j_other/\
+                         job_arrival j_other < job_arrival j/\
+                         job_task j = job_task j_other/\
+                         scheduled_at sched j_other t)).
+
+    Definition Respects_TDMA_policy:=
+      forall (j:Job) (t:time),
+        arrives_in arr_seq j ->
+        sched_implies_in_slot j t /\ backlogged_implies_not_in_slot_or_other_job_sched j t.
+
+  End Properties.
+
+End Platform_TDMA.

model/schedule/uni/end_time.v

+Require Import Arith Nat. 
+Require Import rt.util.all rt.util.tactics_gr.
+Require Import rt.model.arrival.basic.task 
+               rt.model.arrival.basic.job 
+               rt.model.schedule.uni.schedule
+               rt.model.schedule.uni.response_time.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+
+Set Bullet Behavior "Strict Subproofs".
+
+Module end_time.
+  Import UniprocessorSchedule Job ResponseTime.
+
+  Section Task.
+    Context {task: eqType}.
+    Variable task_cost: task -> time.
+    Variable task_period: task -> time.
+    Variable task_deadline: task -> time.
+
+    Context {Job: eqType}.
+    Variable job_arrival: Job -> time.
+    Variable job_cost: Job -> time.
+    Variable job_deadline: Job -> time.
+    Variable job_task: Job -> task.
+
+    (* instant option, to be used in end_time_option *)
+    Inductive diagnosis_option : Set :=
+      | OK      : instant -> diagnosis_option
+      | Failure : instant -> diagnosis_option.
+
+    Section Job_end_time_Def.
+
+      (* Jobs will be scheduled on an uniprocessor *)
+      Variable sched: schedule Job.
+
+      (* Consider any job *)
+      Variable job:Job.
+
+      (* Recall the definition of scheduled_at for testing wether this job can 
+        be scheduled at time t *)
+      Let job_scheduled_at t:= scheduled_at sched job t = true. 
+
+      (* We define the function calculating the job's end time.
+         It takes three arguments:
+         t : job arrival [instant]
+         c : job cost [duration]
+         wf: an extra parameter that allows to realize a well-founded fixpoint
+             with the type [nat]. It is supposed big enough to return the actual end time.
+             Otherwise (i.e., it reaches 0), the function returns Failure t *)
+      Fixpoint end_time_option (t:instant) (c:duration) (wf:nat):=
+        match c with
+        | 0   =>  OK t
+        | S c'=> match wf with
+              | 0    => Failure t
+              | S wf'=> if scheduled_at sched job t then end_time_option  (S t) c' wf'
+                            else end_time_option  (S t) c wf'
+              end
+        end.
+
+      (* We define an end time predicate with three arguments:
+         the job arrival [instant], the job cost [duration] and 
+         the job end time [instant]. Its three constructors 
+         correspond to the cases:
+         - cost = 0 and job has ended
+         - cost > 0 and job cannot be scheduled at instant t
+         - cost > 0 and job can be scheduled at instant t
+      *)
+      Inductive end_time_predicate : instant-> duration->instant->Prop:=
+        |C0_: forall t, end_time_predicate t 0 t
+
+        |S_C_not_sched: forall t c e,  
+          ~job_scheduled_at  t->
+          end_time_predicate  (S t) (S c) e->
+          end_time_predicate  t (S c) e
+
+        |S_C_sched: forall t c e,
+          job_scheduled_at t->
+          end_time_predicate (S t)  c e-> 
+          end_time_predicate  t (S c) e.
+
+      (* The predicate completes_at specifies the instant a job ends
+          according to its arrival and cost *)
+      Definition completes_at (t:instant):=
+        end_time_predicate (job_arrival job) (job_cost job) t.
+
+    End Job_end_time_Def.
+
+    Section Lemmas.
+
+      (* Consider any job *)
+      Variable job:Job.
+
+      (* ... and and uniprocessor schedule this job*)
+      Variable sched: schedule Job.
+
+      (* ... where jobs do not execute before their arrival times nor after completion *)
+      Hypothesis H_jobs_must_arrive_to_execute:
+        jobs_must_arrive_to_execute job_arrival sched.
+      Hypothesis H_completed_jobs_dont_execute:
+        completed_jobs_dont_execute job_cost sched.
+
+      Hypothesis H_valid_job:
+      valid_realtime_job job_cost job_deadline job.
+
+      (* Recall the function end_time_option*)
+      Let job_end_time_function:= end_time_option sched job.
+
+      (* Recall the end time predicate*)
+      Let job_end_time_p:= end_time_predicate sched job.
+
+      (* Recall the definition of completes_at*)
+      Let job_completes_at := completes_at sched job.
+
+      (* Recall the definition of scheduled_at for testing wether this job can 
+        be scheduled at time t.*)
+      Let job_scheduled_at t:= scheduled_at sched job t = true. 
+
+      (* Then, the job_end_time_function (if it terminates successfully) returns
+         the same result as the job_end_time_p predicate *)
+      (* function -> predicate *)
+      Theorem end_time_function_predicat_equivalence:
+        forall e wf t c,
+          job_end_time_function t c wf = OK e ->
+          job_end_time_p t c e.
+      Proof. 
+        induction wf as [| wf' IHwf']; intros t c; simpl.
+        -  destruct c; intros H; inverts H.  
+           apply C0_.
+        -  intros IHSwf. cases (scheduled_at sched job t) as Hcases; destruct c.
+          + inversion IHSwf. apply C0_.
+          + apply IHwf' in IHSwf. apply S_C_sched with (c:=c)(e:=e). 
+            apply Hcases. apply IHSwf.
+          + inversion IHSwf. apply C0_.
+          + apply IHwf' in IHSwf. apply S_C_not_sched with (c:=c)(e:=e). 
+            * rewrite Hcases. done.
+            * apply IHSwf.
+      Qed.
+
+      (* The end time given by the predicate job_end_time_p  is the same as
+         the result returned by the function job_end_time_function (provided
+         wf is large enough) *)
+      Theorem end_time_predicat_function_equivalence:
+        forall t c e ,
+          job_end_time_p t c e ->
+          exists wf, job_end_time_function t c wf = OK e.
+      Proof.
+        intros.
+        induction H as [t|t c e Hcase1 Hpre [wf Hwf] |t c e Hcase2 Hpre [wf Hwf]].
+        - exists 1. done.
+        - exists (1+wf).
+          cases (scheduled_at sched job t) as Csa.
+          + false.
+          + simpl. rewrite Csa. apply Hwf.
+        - exists (1+wf). simpl. 
+          rewrite Hcase2. apply Hwf.
+      Qed.
+
+      (* If we consider a time t where the job is not scheduled, then 
+         the end_time_predicate returns the same end time starting from t or t+1 *)
+      Lemma end_time_predicate_not_sched:
+        forall t c e,
+          ~(job_scheduled_at t) ->
+          end_time_predicate sched job t c.+1 e ->
+          end_time_predicate sched job t.+1 c.+1 e.
+      Proof.
+        intros* Hcase1 Hpre.
+        induction t as [| t' IHt']; 
+        inversion Hpre; try apply H2; false. 
+      Qed.
+
+      (* If we consider a time t where the job is scheduled, then the end_time_predicate 
+         returns the same end time starting from t with a cost c+1 than from t+1 with a cost c*)
+      Lemma end_time_predicate_sched:
+        forall t c e,
+          job_scheduled_at t ->
+          end_time_predicate sched job t c.+1 e ->
+          end_time_predicate sched job t.+1 c e.
+      Proof.
+        intros* Hcase2 Hpre.
+        induction t as [| t' IHt']; 
+        inversion Hpre; try apply H2; false. 
+      Qed.
+
+      (* Assume that the job end time is job_end *)
+      Variable job_end: instant.
+
+      (* Recall the definition of completed_by defined in
+        model/schedule/uni/schedule.v *)
+      Let job_completed_by:=
+        completed_by job_cost sched.
+
+      (* Recall the definition of service_during defined in
+        model/schedule/uni/schedule.v *)
+      Let job_service_during:=
+        service_during sched job.
+
+      (* then the job arrival is less than or equal to job end time *)
+      Lemma arrival_le_end:
+         forall t c e, job_end_time_p t c e -> t <= e.
+      Proof.
+        intros* G.
+        induction G as [t|t c e Hcase1 Hpre |t c e Hcase2 Hpre]; ssromega.
+      Qed.
+
+      (* the sum of job arrival and job cost is less than or equal to 
+        job end time*)
+      Lemma arrival_add_cost_le_end:
+        forall t c e,
+          job_end_time_p t c e ->
+          t+c<=e.
+      Proof.
+        intros* h1.
+        induction h1 as [t|t c e Hcase1 Hpre |t c e Hcase2 Hpre]; ssromega.
+      Qed.
+
+      (* The servive received between the job arrival
+         and the job end is equal to the job cost*)
+      Lemma service_eq_cost_at_end_time:
+        job_completes_at job_end ->
+        job_service_during (job_arrival job) job_end = job_cost job.
+      Proof.
+        intros job_cmplted.
+        induction job_cmplted as [t|t c e Hcase1 Hpre |t c e Hcase2 Hpre];
+        unfold job_service_during, service_during in *.
+        - by rewrite big_geq.
+        - apply arrival_le_end in Hpre.
+          rewrite big_ltn // IHHpre /service_at.
+          cases (scheduled_at sched job t) as cases; try easy; false.
+        - apply arrival_le_end in Hpre. 
+          rewrite big_ltn // IHHpre /service_at. 
+          rewrite Hcase2 //. 
+      Qed.
+
+      (* A job is completed by job end time*)
+      Lemma completed_by_end_time:
+        job_completes_at job_end ->
+        job_completed_by job job_end.
+      Proof.
+        intro job_cmplted.
+        unfold job_completed_by, completed_by, service, service_during. 
+        rewrite (ignore_service_before_arrival job_arrival sched ) //. 
+        - apply service_eq_cost_at_end_time in job_cmplted. 
+          by apply /eqP.
+        - by apply arrival_le_end in job_cmplted.
+      Qed.
+
+      (* The job end time is positive *)
+      Corollary end_time_positive:
+        job_completes_at job_end -> job_end > 0.
+      Proof.
+        intro h1. 
+        assert (H_slot: job_cost job > 0) by (apply H_valid_job).
+        apply completed_by_end_time in h1.
+        unfold job_completed_by, completed_by, service, service_during in h1.
+        destruct job_end; trivial. 
+        rewrite big_geq // in h1. 
+        ssromega.
+      Qed.
+
+      (* The service received between job arrival and the previous instant
+         of job end time is exactly job cost-1*)
+      Lemma job_uncompletes_at_end_time_sub_1:
+        job_completes_at job_end ->
+        job_service_during (job_arrival job) (job_end .-1) = (job_cost job) .-1.
+      Proof.
+        intros job_cmplted.
+        induction job_cmplted as [t|t c e Hcase1 Hpre |t c e Hcase2 Hpre];
+        unfold job_service_during, service_during in*.
+        - apply big_geq, leq_pred. 
+        - apply arrival_add_cost_le_end, leq_sub2r with (p:=1) in Hpre.
+          rewrite subn1 addnS //= addSn subn1 in Hpre.
+          apply leq_ltn_trans with (m:=t) in Hpre; try (apply leq_addr).
+          rewrite big_ltn // IHHpre /service_at /service_during.
+          cases (scheduled_at sched job t). false. done.  
+        - destruct c. 
+          + inversion Hpre. apply big_geq. ssromega.
+          + apply arrival_add_cost_le_end, leq_sub2r with (p:=1) in Hpre.
+            rewrite subn1 addnS //= addSn subn1 in Hpre.
+            apply leq_ltn_trans with (m:=t) in Hpre; try (apply leq_addr).
+            rewrite big_ltn // /service_at / service_during IHHpre Hcase2 //.
+      Qed.
+
+      (* At any instant from the job arrival and before the job end time,
+         job cannot be finished; the service received is always less than job cost*)
+      Lemma job_uncompleted_before_end_time:
+        job_completes_at job_end ->
+        forall t', job_arrival job <= t' /\ t'<= job_end.-1 -> 
+           job_service_during (job_arrival job) t' < job_cost job.
+      Proof.
+        intros job_cmplted t' [ht1 ht2].
+        assert (H_slot: job_cost job > 0) by (apply H_valid_job).
+        apply leq_ltn_trans with (n:= (job_cost job).-1); last ssromega.
+        rewrite -job_uncompletes_at_end_time_sub_1 // /job_service_during /service_during.
+        assert (H_lt: exists delta, t' + delta = job_end.-1).
+        - move/leP:ht2 => ht2.
+          apply Nat.le_exists_sub in ht2.
+          destruct ht2 as [p [ht21 ht22]]. exists p. ssromega.
+        - destruct H_lt as [delta ht']. rewrite -ht'.
+          replace (\sum_(job_arrival job <= t < t' + delta) service_at sched job t)
+          with    (addn_monoid(\big[addn_monoid/0]_(job_arrival job <= i < t') service_at sched job i)
+                  (\big[addn_monoid/0]_(t'  <= i < t'+delta) service_at sched job i)); simpl; try ssromega.
+          symmetry. apply big_cat_nat; ssromega.
+      Qed.
+
+    End Lemmas.
+
+  End Task.
+
+End end_time.
\ No newline at end of file

model/time.v

@@ -2,5 +2,7 @@ Module Time.
 
   (* Time is defined as a natural number. *)
   Definition time := nat.
+  Definition duration := time.
+  Definition instant  := time.
 
 End Time.
\ No newline at end of file

util/find_seq.v

+From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq bigop div.
+Require Import rt.util.all. 
+
+Section find_seq.
+  Context {T:eqType}.
+  Variable P: T-> bool.
+  Fixpoint findP l:= 
+    match l with 
+    | nil => None
+    | x::s => if P x then Some x else findP s
+    end.
+
+  Lemma findP_FIFO:
+    forall (l:seq T) x y,
+    P y = true -> y \in l -> x <> y ->
+    findP l = Some x ->
+    find (fun j => j==x) l < find (fun j => j==y) l.
+  Proof.
+    intros* PY YIN NEQ FIND.
+    induction l.
+    - auto.
+    - case (a==x)eqn:AX;case (a==y)eqn:AY;simpl; rewrite AX AY;auto.
+      + move/eqP in AX;move/eqP in AY;rewrite AX in AY;auto.
+      + simpl in FIND;move/eqP in AY;rewrite AY PY in FIND;clarify;
+        by move/eqP in AX. 
+      + rewrite in_cons in YIN. move:YIN=> /orP [/eqP EQ | YIN]. move/eqP in AY;auto.
+        simpl in FIND. case (P a) eqn:PA;clarify. move/eqP in AX;auto. apply IHl;auto.
+  Qed.
+
+  Lemma find_uniql:
+    forall (x:T) l1 l2,
+    uniq(l1 ++ l2) ->
+    x \in l2 ->
+    ~ x \in l1.
+  Proof.
+    intros. intro XIN.
+    induction l1. auto. 
+    case (a==x)eqn:AX;move/eqP in AX;simpl in H;
+    move:H=>/andP [NIN U];move/negP in NIN;auto.
+    rewrite AX in NIN. have XIN12: x \in (l1++l2).
+    rewrite mem_cat. apply/orP. by right.
+    apply IHl1;auto. rewrite in_cons in XIN.
+    move:XIN=>/orP [/eqP EQ | XL1];auto.
+  Qed.
+
+  Lemma find_uniq:
+    forall (x:T) l1 l2,
+    uniq(l1 ++ l2) ->
+    x \in l2 ->
+    has (fun x': T=> x'==x) l1 = false.
+  Proof.
+    intros.
+    apply /negP /negP /hasPn.
+    intros. apply find_uniql with (x:=x) in H;auto.
+    case (x0==x)eqn:XX;move/eqP in XX;last trivial.
+    rewrite -XX in H0. by subst.
+  Qed.
+
+  Lemma findP_in_seq:
+    forall (l:seq T) x,
+    findP l = Some x ->
+    P x /\ x \in l.
+  Proof.
+    intros* FIND.
+    split.
+    - generalize dependent x. induction l.
+      + by rewrite /=.
+      + simpl. case (P a) eqn:CASE. intros x SOME.
+        case : SOME => AX. subst. auto.
+        assumption.
+    - generalize dependent x. induction l.
+      + by rewrite /=.
+      + simpl. case (P a) eqn:CASE. intros x SOME.
+        case : SOME => AX. subst. rewrite in_cons.
+        apply/orP. left. trivial.
+        intros x FIND. rewrite in_cons. apply/orP. right. auto.
+  Qed.
+
+  Lemma findP_notSome_in_seq:
+    forall (l:seq T) x,
+    findP l != Some x ->
+    x \in l->
+    ~ P x \/ exists y, findP l = Some y.
+  Proof.
+    intros* NFIND IN.
+    generalize dependent x. induction l;intros x G IN.
+    - auto.
+    - simpl in G. case (P a) eqn:CASE.
+      + right;exists a;simpl;by rewrite CASE.
+      + case (a==x) eqn:AX.
+        * left. move/eqP in AX. by rewrite -AX CASE.
+        * apply IHl in G. destruct G as [NP|EXIST].
+          -- by left.
+          -- right. simpl. by rewrite CASE. 
+             rewrite in_cons in IN. move/orP in IN.
+             destruct IN as [XA | XINL].
+             ++ move/eqP in XA. move/eqP in AX. auto.
+             ++ trivial.
+   Qed.
+
+End find_seq.
+
+
+