diff --git a/model/schedule/uni/nonpreemptive/platform.v b/model/schedule/uni/nonpreemptive/platform.v
new file mode 100644
index 0000000000000000000000000000000000000000..45b8a76f6230a758ccf1433df52f9951e40a9be9
--- /dev/null
+++ b/model/schedule/uni/nonpreemptive/platform.v
@@ -0,0 +1,121 @@
+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.
+Require Import rt.model.schedule.uni.schedule
+ rt.model.schedule.uni.basic.platform.
+Require Import rt.model.schedule.uni.nonpreemptive.schedule.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
+
+Module NonpreemptivePlatform.
+
+ Import Job SporadicTaskset UniprocessorSchedule Priority.
+
+ (* In this section, we define properties of the processor platform. *)
+ Section Properties.
+
+ Context {sporadic_task: eqType}.
+
+ Context {Job: eqType}.
+ Variable job_arrival: Job -> time.
+ Variable job_cost: Job -> time.
+ Variable job_task: Job -> sporadic_task.
+
+ (* Consider any job arrival sequence ...*)
+ Variable arr_seq: arrival_sequence Job.
+
+ (* ...and any uniprocessor schedule of these jobs. *)
+ Variable sched: schedule Job.
+
+ (* For simplicity, let's define some local names. *)
+ Let job_completed_by := completed_by job_cost sched.
+ Let job_scheduled_at := scheduled_at sched.
+
+ (* First, we define the notion of a preemption point. *)
+ Section PreemptionPoint.
+
+ (* We say that t is a preemption point iff (a) t is equal to 0
+ or (b) there is no scheduling job at time t or
+ (c) a job that was scheduled at time (t - 1) and
+ has completed by t exists. *)
+ Definition is_preemption_point' (t: time) :=
+ t = 0
+ \/ sched (t-1) = None
+ \/ exists j, scheduled_at sched j (t - 1) /\ job_completed_by j t.
+
+ (* Moreover, we provide a shorter definition, more convenient for the proofs. *)
+ Definition is_preemption_point (t: time) :=
+ t = 0 \/ forall j, job_scheduled_at j (t - 1) -> job_completed_by j t.
+
+ (* Let's prove that the definitions above are equal. *)
+ Lemma defitions_of_preemption_point_are_equal:
+ forall t, is_preemption_point t <-> is_preemption_point' t.
+ Proof.
+ unfold is_preemption_point, is_preemption_point'.
+ intros; split; intros.
+ {
+ destruct H as [H | H]; [by left | right].
+ destruct (sched (t-1)) eqn:SCHED; [right; exists s | by left].
+ move: SCHED => /eqP SCHED.
+ by split; last by apply H in SCHED.
+ }
+ {
+ destruct H as [H | [H | H]]; [by left| | ]; right; intros.
+ unfold job_scheduled_at, scheduled_at in H0. rewrite H in H0. inversion H0.
+ inversion H as [j' [H1 H2]]. unfold job_scheduled_at in H0.
+ have EQ: j = j'. by apply (only_one_job_scheduled sched) with (t := t-1).
+ by subst j'.
+ }
+ Qed.
+
+ End PreemptionPoint.
+
+ (* Next, we define properties related to execution. *)
+ Section Execution.
+
+ (* We say that a scheduler is work-conserving iff whenever a job j
+ is backlogged, the processor is always busy with another job. *)
+ (* Imported from the preemptive schedule. *)
+ Definition work_conserving := Platform.work_conserving job_cost.
+
+ End Execution.
+
+ (* Next, we define properties related to FP scheduling. *)
+ Section FP.
+
+ (* We say that an FP policy...*)
+ Variable higher_eq_priority: FP_policy sporadic_task.
+
+ (* ...is respected by the schedule iff a scheduled task has
+ higher (or same) priority than (as) any backlogged task at
+ every preemption point. *)
+ Definition respects_FP_policy_at_preemption_point :=
+ forall j j_hp t,
+ arrives_in arr_seq j ->
+ backlogged job_arrival job_cost sched j t ->
+ scheduled_at sched j_hp t ->
+ is_preemption_point t ->
+ higher_eq_priority (job_task j_hp) (job_task j).
+
+ End FP.
+
+ (* Next, we define properties related to JLFP policies. *)
+ Section JLFP.
+
+ (* We say that a JLFP policy ...*)
+ Variable higher_eq_priority: JLFP_policy Job.
+
+ (* ... is respected by the scheduler iff a scheduled job has
+ higher (or same) priority than (as) any backlogged job at
+ every preemption point. *)
+ Definition respects_JLFP_policy_at_preemption_point :=
+ forall j j_hp t,
+ arrives_in arr_seq j ->
+ backlogged job_arrival job_cost sched j t ->
+ scheduled_at sched j_hp t ->
+ is_preemption_point t ->
+ higher_eq_priority j_hp j.
+
+ End JLFP.
+
+ End Properties.
+
+End NonpreemptivePlatform.
\ No newline at end of file
diff --git a/model/schedule/uni/nonpreemptive/schedule.v b/model/schedule/uni/nonpreemptive/schedule.v
new file mode 100644
index 0000000000000000000000000000000000000000..8d867d4f2137853f230e24a1a95cde02fdf101ec
--- /dev/null
+++ b/model/schedule/uni/nonpreemptive/schedule.v
@@ -0,0 +1,381 @@
+Require Import rt.util.all.
+Require Import rt.model.arrival.basic.job.
+Require Import rt.model.schedule.uni.schedule.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+
+Module NonpreemptiveSchedule.
+
+ Export UniprocessorSchedule.
+
+ Section Definitions.
+
+ Context {Job: eqType}.
+ Variable job_arrival: Job -> time.
+ Variable job_cost: Job -> time.
+
+ (* Consider any uniprocessor schedule. *)
+ Variable sched: schedule Job.
+
+ (* For simplicity, let's define some local names. *)
+ Let job_completed_by := completed_by job_cost sched.
+ Let job_remaining_cost j t := remaining_cost job_cost sched j t.
+
+ (* We define schedule to be nonpreemptive iff every job remains scheduled until completion. *)
+ Definition is_nonpreemptive_schedule :=
+ forall j t t',
+ t <= t' ->
+ scheduled_at sched j t ->
+ ~~ job_completed_by j t' ->
+ scheduled_at sched j t'.
+
+ (* In this section, we prove some basic lemmas about nonpreemptive schedules. *)
+ Section Lemmas.
+
+ (* Assume that we have a nonpreemptive schedule. *)
+ Hypothesis H_nonpreemptive: is_nonpreemptive_schedule.
+
+ Section BasicLemmas.
+
+ (* Consider any job j. *)
+ Variable j: Job.
+
+ (* Assume that completed jobs do not execute. *)
+ Hypothesis H_completed_jobs_dont_execute:
+ completed_jobs_dont_execute job_cost sched.
+
+ (* First, we show that if j is scheduled at any two time instants,
+ then it is also scheduled at any time between them. *)
+ Lemma continuity_of_nonpreemptive_scheduling:
+ forall t t1 t2,
+ t1 <= t <= t2 ->
+ scheduled_at sched j t1 ->
+ scheduled_at sched j t2 ->
+ scheduled_at sched j t.
+ Proof.
+ move => t t1 t2 /andP [GT LE] SCHEDt1 SCHEDt2.
+ unfold is_nonpreemptive_schedule, job_completed_by in *.
+ apply H_nonpreemptive with (t := t1); [by done| by done| ].
+ apply /negP; intros COMP.
+ apply (scheduled_implies_not_completed job_cost) in SCHEDt2; last by done.
+ apply completion_monotonic with (t' := t2) in COMP; [ |by done| by done].
+ by move: SCHEDt2 => /negP SCHEDt2; apply: SCHEDt2.
+ Qed.
+
+ (* Next, we show that in any nonpreemptive schedule, once a job is scheduled,
+ it cannot be preempted until completion. *)
+ Lemma in_nonpreemption_schedule_preemption_implies_completeness:
+ forall t t' ,
+ t <= t' ->
+ scheduled_at sched j t ->
+ ~~ scheduled_at sched j t' ->
+ job_completed_by j t'.
+ Proof.
+ intros t t' LE SCHED; apply contraNT.
+ by apply H_nonpreemptive with (t := t).
+ Qed.
+
+ End BasicLemmas.
+
+ (* In this section, we prove properties related to job completion. *)
+ Section CompletionUnderNonpreemptive.
+
+ (* Assume that completed jobs do not execute. *)
+ Hypothesis H_completed_jobs_dont_execute:
+ completed_jobs_dont_execute job_cost sched.
+
+ (* If job j is scheduled at time t, then it must complete by (t + remaining_cost j t). *)
+ Lemma job_completes_after_remaining_cost:
+ forall j t,
+ scheduled_at sched j t ->
+ job_completed_by j (t + job_remaining_cost j t).
+ Proof.
+ intros j t SCHED.
+ rewrite /job_completed_by /completed_by eqn_leq.
+ apply /andP; split;
+ first by apply cumulative_service_le_job_cost.
+ rewrite /service /service_during.
+ rewrite (@big_cat_nat _ _ _ t) //= ?leq_addr //.
+ apply leq_trans with (n := service sched j t + job_remaining_cost j t);
+ first by rewrite /remaining_cost subnKC //.
+ rewrite leq_add2l.
+ set t2 := t + _.
+ apply leq_trans with (n := \sum_(t <= i < t2) 1);
+ first by simpl_sum_const; rewrite /t2 addKn.
+ apply leq_sum_nat.
+ move => i /andP [GE LT _].
+ rewrite lt0n eqb0 negbK.
+ apply (H_nonpreemptive j t i); try (by done).
+ unfold t2 in *; clear t2.
+ have NOTCOMP: ~~ job_completed_by j t.
+ {
+ apply contraT. rewrite negbK. intros COMP.
+ apply completed_implies_not_scheduled in COMP; last by done.
+ by rewrite SCHED in COMP.
+ }
+ apply job_doesnt_complete_before_remaining_cost in NOTCOMP; last by done.
+ apply contraT; rewrite negbK; intros COMP.
+ exfalso; move: NOTCOMP => /negP NOTCOMP; apply: NOTCOMP.
+ apply completion_monotonic with (t0 := i); try ( by done).
+ apply subh3; first by rewrite addn1.
+ by apply leq_ltn_trans with (n := i).
+ Qed.
+
+ End CompletionUnderNonpreemptive.
+
+ (* In this section, we determine bounds on the length of the execution interval. *)
+ Section ExecutionInterval.
+
+ (* Assume that jobs do not execute after completion. *)
+ Hypothesis H_completed_jobs_dont_execute:
+ completed_jobs_dont_execute job_cost sched.
+
+ (* Let j be any job scheduled at time t. *)
+ Variable j: Job.
+ Variable t: time.
+ Hypothesis H_j_is_scheduled_at_t: scheduled_at sched j t.
+
+ (* Is this section we show that there is a bound for how early job j can start. *)
+ Section LeftBound.
+
+ (* We prove that job j is scheduled at time (t - service sched j t)... *)
+ Lemma j_is_scheduled_at_t_minus_service:
+ scheduled_at sched j (t - service sched j t).
+ Proof.
+ unfold is_nonpreemptive_schedule in *.
+ apply contraT; intros CONTRA; exfalso.
+ rename H_j_is_scheduled_at_t into SCHED.
+
+ have COSTPOS: job_cost j > 0.
+ {
+ apply (scheduled_implies_not_completed job_cost) in SCHED.
+ unfold job_completed_by, completed_by in SCHED.
+ apply contraT; rewrite -eqn0Ngt.
+ move => /eqP EQ0.
+ rewrite EQ0 in SCHED.
+ move: SCHED => /eqP GT0.
+ exfalso; apply: GT0; apply /eqP.
+ rewrite eqn_leq.
+ apply /andP; split; last by done.
+ rewrite -EQ0.
+ apply H_completed_jobs_dont_execute.
+ by done.
+ }
+
+ have H := job_completes_after_remaining_cost
+ H_completed_jobs_dont_execute
+ j t SCHED.
+
+ unfold job_completed_by, completed_by in H.
+ move: H => /eqP H.
+
+ unfold service, service_during in H.
+
+ rewrite
+ (@big_cat_nat _ _ _ (t - service sched j t)) //= in H;
+ last by rewrite leq_subLR addnC -addnA leq_addr.
+ have R: forall a b c, a + b = c -> b < c -> a > 0.
+ {
+ by intros a b c EQ LT; induction a;
+ first by rewrite add0n in EQ; subst b;
+ rewrite ltnn in LT.
+ }
+
+ apply R in H; last first.
+ {
+ have CUMLED := cumulative_service_le_delta sched j 0 t.
+ have CUMLEJC := cumulative_service_le_job_cost _ _ H_completed_jobs_dont_execute j 0 t.
+ rewrite (@big_cat_nat _ _ _ ((t - service sched j t).+1)) //=.
+ {
+ rewrite big_nat_recl; last by done.
+ rewrite big_geq; last by done.
+ rewrite -eqb0 in CONTRA; move: CONTRA => /eqP CONTRA.
+ rewrite /service_at CONTRA add0n add0n.
+
+ apply leq_ltn_trans with
+ (t + job_remaining_cost j t - ((t - service sched j t).+1));
+ first by rewrite cumulative_service_le_delta'.
+ unfold remaining_cost.
+ rewrite -addn1 -addn1 subh1; first by
+ by rewrite leq_subLR addnBA;
+ first by rewrite -addnA [1+job_cost j]addnC addnA -subh1.
+ {
+ rewrite subh1; last by done.
+ rewrite leq_subLR addnA.
+ rewrite addnBA; last by done.
+ rewrite [_+t]addnC [_+job_cost j]addnC addnA.
+ rewrite -addnBA; last by done.
+ by rewrite subnn addn0 addnC leq_add2r.
+ }
+ }
+ {
+ unfold remaining_cost.
+ rewrite addnBA; last by done.
+ rewrite -addn1 subh1; last by done.
+ rewrite leq_subLR -addnBA; last by done.
+ rewrite addnA [_+t]addnC -addnA leq_add2l addnBA; last by done.
+ by rewrite addnC -addnBA; first by rewrite subnn addn0.
+ }
+ }
+ {
+ rewrite lt0n in H; move: H => /neqP H; apply: H.
+ rewrite big_nat_cond big1 //; move => i /andP [/andP [_ LT] _].
+ apply /eqP; rewrite eqb0; apply /negP; intros CONT.
+
+ have Y := continuity_of_nonpreemptive_scheduling j _ (t - service sched j t) i t.
+ feed_n 4 Y; try(done).
+ by apply/andP; split; [rewrite ltnW | rewrite leq_subr].
+ by move: CONTRA => /negP CONTRA; apply CONTRA.
+ }
+ Qed.
+
+ (* ... and it is not scheduled at time (t - service sched j t - 1). *)
+ Lemma j_is_not_scheduled_at_t_minus_service_minus_one:
+ t - service sched j t > 0 ->
+ ~~ scheduled_at sched j (t - service sched j t - 1).
+ Proof.
+ rename H_j_is_scheduled_at_t into SCHED.
+ intros GT; apply/negP; intros CONTRA.
+
+ have L1 := job_doesnt_complete_before_remaining_cost
+ job_cost sched H_completed_jobs_dont_execute
+ j t.
+ feed L1; first by rewrite scheduled_implies_not_completed.
+
+ have L2 := job_completes_after_remaining_cost
+ H_completed_jobs_dont_execute
+ j (t-service sched j t - 1).
+ feed L2; first by done.
+
+ have EQ:
+ t + job_remaining_cost j t - 1 =
+ t - service sched j t - 1 + job_remaining_cost j (t - service sched j t - 1).
+ {
+ have T1: service sched j (t - service sched j t - 1) = 0.
+ {
+
+ rewrite [service _ _ _]/service /service_during.
+ rewrite big_nat_cond big1 //; move => t' /andP [/andP [_ LT] _].
+ apply /eqP; rewrite eqb0; apply /negP; intros CONTR.
+
+ have COMPL: completed_by job_cost sched j (t + job_remaining_cost j t - 1).
+ {
+ apply completion_monotonic with (t0 := t' + job_remaining_cost j t');
+ [by done | | by apply job_completes_after_remaining_cost].
+
+ unfold remaining_cost.
+
+ have LLF: t' < t - service sched j t.
+ {
+ by apply ltn_trans with (t - service sched j t - 1);
+ last by rewrite -addn1 subh1 // -addnBA // subnn addn0.
+ } clear LT.
+
+ rewrite !addnBA;
+ try(rewrite H_completed_jobs_dont_execute //).
+ rewrite [t' + _]addnC [t + _]addnC.
+ rewrite -addnBA; last by rewrite cumulative_service_le_delta.
+ rewrite -addnBA; last by rewrite cumulative_service_le_delta.
+ rewrite -addnBA ?leq_add2l; last by done.
+ by apply leq_trans with (t' + 1 - 1);
+ rewrite addn1 subn1 -pred_Sn;
+ [rewrite leq_subr | rewrite subh3 // addn1].
+ }
+
+ have L3 := job_doesnt_complete_before_remaining_cost job_cost sched
+ H_completed_jobs_dont_execute j t;
+ feed L3; first by rewrite scheduled_implies_not_completed.
+ unfold job_completed_by in *.
+ by move: L3 => /negP L3; apply L3.
+ }
+ rewrite /job_remaining_cost /remaining_cost T1 subn0 addnBA; last by done.
+ rewrite -subh1.
+ by rewrite -[(t-service sched j t) + _ - _]subh1.
+ by rewrite cumulative_service_le_delta.
+ }
+ move: L1 => /neqP L1; apply: L1.
+ rewrite -EQ in L2.
+ by unfold job_completed_by, completed_by in L2; move: L2 => /eqP L2.
+ Qed.
+
+ (* Using the previous lemma, we show that job j cannot be scheduled
+ before (t - service sched j t). *)
+ Lemma j_is_not_scheduled_earlier_t_minus_service:
+ forall t',
+ t' < t - service sched j t ->
+ ~~ scheduled_at sched j t'.
+ Proof.
+ intros t' GT.
+ have NOTSCHED := j_is_not_scheduled_at_t_minus_service_minus_one;
+ feed NOTSCHED; first by apply leq_ltn_trans with t'.
+ apply/negP; intros CONTRA.
+ move: NOTSCHED => /negP NOTSCHED; apply: NOTSCHED.
+ apply continuity_of_nonpreemptive_scheduling with (t1 := t') (t2 := t);
+ [ by done | | by done | by done ].
+ apply/andP; split; last by apply leq_trans with (t - service sched j t); rewrite leq_subr.
+ rewrite [t']pred_Sn -subn1 leq_sub2r //.
+ Qed.
+
+ End LeftBound.
+
+ (* Is this section we prove that job j cannot be scheduled after (t + remaining_cost j t - 1). *)
+ Section RightBound.
+
+ (* We show that if job j is scheduled at time t,
+ then it is also scheduled at time (t + remaining_cost j t - 1)... *)
+ Lemma j_is_scheduled_at_t_plus_remaining_cost_minus_one:
+ scheduled_at sched j (t + job_remaining_cost j t - 1).
+ Proof.
+ move: (H_j_is_scheduled_at_t) => COMP.
+ apply (scheduled_implies_not_completed job_cost) in COMP; last by done.
+ apply job_doesnt_complete_before_remaining_cost in COMP; last by done.
+ move: COMP; apply contraR; intros CONTR.
+ apply in_nonpreemption_schedule_preemption_implies_completeness
+ with (t:=t); [|by done| by done].
+ rewrite subh3 // ?leq_add2l;
+ first by rewrite scheduled_implies_positive_remaining_cost //.
+ rewrite addn_gt0; apply/orP; right;
+ rewrite scheduled_implies_positive_remaining_cost //.
+ Qed.
+
+ (* ... and it is not scheduled after (t + remaining cost j t - 1). *)
+ Lemma j_is_not_scheduled_after_t_plus_remaining_cost_minus_one:
+ forall t',
+ t + job_remaining_cost j t <= t' ->
+ ~~ scheduled_at sched j t'.
+ Proof.
+ intros t' GE.
+ unfold job_completed_by in *.
+ rename H_j_is_scheduled_at_t into SCHED.
+ apply job_completes_after_remaining_cost in SCHED; last by done.
+ by apply (completion_monotonic job_cost) with (t' := t') in SCHED; first
+ by apply (completed_implies_not_scheduled job_cost).
+ Qed.
+
+ End RightBound.
+
+ (* To conclude, we identify the interval where job j is scheduled. *)
+ Lemma nonpreemptive_executing_interval:
+ forall t',
+ t - service sched j t <= t' < t + job_remaining_cost j t ->
+ scheduled_at sched j t'.
+ Proof.
+ move => t' /andP [GE LE].
+ move: (H_j_is_scheduled_at_t) => SCHED1; move: (H_j_is_scheduled_at_t) => SCHED2.
+ rewrite -addn1 in LE; apply subh3 with (m := t') (p := 1) in LE;
+ last by rewrite addn_gt0; apply/orP; right;
+ rewrite scheduled_implies_positive_remaining_cost //.
+ apply continuity_of_nonpreemptive_scheduling with
+ (t1 := t - service sched j t)
+ (t2 := t + job_remaining_cost j t - 1); first by done.
+ - by apply/andP;split.
+ - by apply j_is_scheduled_at_t_minus_service.
+ - by apply j_is_scheduled_at_t_plus_remaining_cost_minus_one.
+ Qed.
+
+ End ExecutionInterval.
+
+ End Lemmas.
+
+ End Definitions.
+
+End NonpreemptiveSchedule.
\ No newline at end of file