diff --git a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.v b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.v
index 719cb129f093a54c2dd51f0b3b06c44441c82115..36179365d8096eda956906e90636e3d857458286 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.v
@@ -11,7 +11,7 @@ Require Import rt.restructuring.model.preemption.floating.
 Require Import rt.restructuring.model.schedule.work_conserving.
 Require Import rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.model.priority.edf.
-Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
+Require Import rt.restructuring.model.schedule.priority_driven.
 Require Import rt.restructuring.analysis.arrival.workload_bound.
 Require Import rt.restructuring.analysis.arrival.rbf.
 Require Import rt.restructuring.analysis.edf.rta.nonpr_reg.response_time_bound.
diff --git a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.v b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.v
index 23893b26d05252ff8d5e8ba9622d6b9947b6214c..1d743f001d2e68fcc0cb1776a4b456d2fe088929 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.v
@@ -11,7 +11,7 @@ Require Import rt.restructuring.model.preemption.limited.
 Require Import rt.restructuring.model.schedule.work_conserving.
 Require Import rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.model.priority.edf.
-Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
+Require Import rt.restructuring.model.schedule.priority_driven.
 Require Import rt.restructuring.analysis.arrival.workload_bound.
 Require Import rt.restructuring.analysis.arrival.rbf.
 Require Import rt.restructuring.analysis.edf.rta.nonpr_reg.response_time_bound.
diff --git a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v
index 80a48950483cc40b75fdb398cd335715ced0c34f..e5536a8806c9b76f43eaec9bcf96afe7460da384 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v
@@ -10,7 +10,7 @@ Require Import rt.restructuring.model.arrival.arrival_curves.
 Require Import rt.restructuring.model.schedule.work_conserving.
 Require Import rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.model.priority.edf.
-Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
+Require Import rt.restructuring.model.schedule.priority_driven.
 Require Import rt.restructuring.analysis.arrival.workload_bound.
 Require Import rt.restructuring.analysis.arrival.rbf.
 Require Import rt.restructuring.analysis.edf.rta.nonpr_reg.response_time_bound.
diff --git a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v
index d8d5d1e7ea46e02e58937e74cc4a6e5ed65efca1..a01366022a64e104baf666f6c6902fa9bd47647f 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v
@@ -10,7 +10,7 @@ Require Import rt.restructuring.model.arrival.arrival_curves.
 Require Import rt.restructuring.model.schedule.work_conserving.
 Require Import rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.model.priority.edf.
-Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
+Require Import rt.restructuring.model.schedule.priority_driven.
 Require Import rt.restructuring.analysis.arrival.workload_bound.
 Require Import rt.restructuring.analysis.arrival.rbf.
 Require Import rt.restructuring.analysis.edf.rta.nonpr_reg.response_time_bound.
diff --git a/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v b/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v
index 55ecf77dce5a8ab95929f66ee9c46342bd281cb7..e44a589f4f55604231eb186984209ca19deea723 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v
@@ -16,7 +16,7 @@ Require Import rt.restructuring.analysis.facts.priority_inversion_is_bounded.
 Require Import rt.restructuring.model.schedule.work_conserving.
 Require Import rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.model.priority.edf.
-Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
+Require Import rt.restructuring.model.schedule.priority_driven.
 Require Import rt.restructuring.analysis.arrival.workload_bound.
 Require Import rt.restructuring.analysis.arrival.rbf.
 Require Export rt.restructuring.analysis.edf.rta.response_time_bound.
diff --git a/restructuring/analysis/edf/rta/response_time_bound.v b/restructuring/analysis/edf/rta/response_time_bound.v
index 4c5a3284f48ce311d8b403f5f109ad04e2646f3d..5eb78f449862c351cff7ee5bfcc71d6548028dca 100644
--- a/restructuring/analysis/edf/rta/response_time_bound.v
+++ b/restructuring/analysis/edf/rta/response_time_bound.v
@@ -16,7 +16,7 @@ Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.jo
 Require Import rt.restructuring.model.schedule.work_conserving.
 Require Import rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.model.priority.edf.
-Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
+Require Import rt.restructuring.model.schedule.priority_driven.
 Require Import rt.restructuring.analysis.arrival.workload_bound.
 Require Import rt.restructuring.analysis.arrival.rbf.
 Require Export rt.restructuring.analysis.schedulability.
diff --git a/restructuring/analysis/facts/priority_inversion_is_bounded.v b/restructuring/analysis/facts/priority_inversion_is_bounded.v
index 9e7880b5648255ffe036ca2d29d4f9a9042a5483..771e3324d42240d77517fbcf406f534a0d7ed4c2 100644
--- a/restructuring/analysis/facts/priority_inversion_is_bounded.v
+++ b/restructuring/analysis/facts/priority_inversion_is_bounded.v
@@ -5,7 +5,7 @@ Require Import rt.restructuring.model.preemption.valid_model.
 Require Import rt.restructuring.model.preemption.preemption_time.
 Require Import rt.restructuring.model.preemption.job.parameters.
 Require Import rt.restructuring.model.preemption.task.parameters.
-Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
+Require Import rt.restructuring.model.schedule.priority_driven.
 Require Export rt.restructuring.analysis.definitions.no_carry_in.
 Require Export rt.restructuring.analysis.definitions.busy_interval.
 Require Export rt.restructuring.analysis.definitions.priority_inversion.
diff --git a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/floating.v b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/floating.v
index 3f15c28b0518254679e5f16777cf714de0c3fc7c..1a61e9aff57f1717831014bd159c31ea07d1742b 100644
--- a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/floating.v
+++ b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/floating.v
@@ -10,7 +10,7 @@ Require Import rt.restructuring.model.arrival.arrival_curves.
 Require Import rt.restructuring.model.preemption.floating.
 Require Import rt.restructuring.model.schedule.work_conserving.
 Require Import rt.restructuring.model.priority.classes.
-Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
+Require Import rt.restructuring.model.schedule.priority_driven.
 Require Import rt.restructuring.analysis.arrival.workload_bound.
 Require Import rt.restructuring.analysis.arrival.rbf.
 Require Import rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.response_time_bound.
diff --git a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/limited.v b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/limited.v
index fe73e59a1a126fdfebdf8480883dfc52a56c4ac5..05213cf7e215b21a172665c4112adeb2d0a623e1 100644
--- a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/limited.v
+++ b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/limited.v
@@ -10,7 +10,7 @@ Require Import rt.restructuring.model.arrival.arrival_curves.
 Require Import rt.restructuring.model.preemption.limited.
 Require Import rt.restructuring.model.schedule.work_conserving.
 Require Import rt.restructuring.model.priority.classes.
-Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
+Require Import rt.restructuring.model.schedule.priority_driven.
 Require Import rt.restructuring.analysis.arrival.workload_bound.
 Require Import rt.restructuring.analysis.arrival.rbf.
 Require Import rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.response_time_bound.
diff --git a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/nonpreemptive.v b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/nonpreemptive.v
index 78c93cd0645d088a677f8a036a3ece81ee5c6cd9..58a8bbad0d285858473e899a1f12ad267e9fc339 100644
--- a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/nonpreemptive.v
+++ b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/nonpreemptive.v
@@ -9,7 +9,7 @@ Require Import rt.restructuring.model.readiness.basic.
 Require Import rt.restructuring.model.arrival.arrival_curves.
 Require Import rt.restructuring.model.schedule.work_conserving.
 Require Import rt.restructuring.model.priority.classes.
-Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
+Require Import rt.restructuring.model.schedule.priority_driven.
 Require Import rt.restructuring.analysis.arrival.workload_bound.
 Require Import rt.restructuring.analysis.arrival.rbf.
 Require Import rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.response_time_bound.
diff --git a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/preemptive.v b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/preemptive.v
index 565952da95d9e2bdd959df561d4556403615af98..70cefe5ca889d0f6868ce0deb790de93ea65b8e8 100644
--- a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/preemptive.v
+++ b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/preemptive.v
@@ -9,7 +9,7 @@ Require Import rt.restructuring.model.readiness.basic.
 Require Import rt.restructuring.model.arrival.arrival_curves.
 Require Import rt.restructuring.model.schedule.work_conserving.
 Require Import rt.restructuring.model.priority.classes.
-Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
+Require Import rt.restructuring.model.schedule.priority_driven.
 Require Import rt.restructuring.analysis.arrival.workload_bound.
 Require Import rt.restructuring.analysis.arrival.rbf.
 Require Import rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.response_time_bound.
diff --git a/restructuring/analysis/fixed_priority/rta/nonpr_reg/response_time_bound.v b/restructuring/analysis/fixed_priority/rta/nonpr_reg/response_time_bound.v
index 1b91e8ccf26e4a6676fab408d7b4417ae33b2e3a..ffec52ae669ba2fdaf1cc0ee7b7d88729a74f6d1 100644
--- a/restructuring/analysis/fixed_priority/rta/nonpr_reg/response_time_bound.v
+++ b/restructuring/analysis/fixed_priority/rta/nonpr_reg/response_time_bound.v
@@ -13,7 +13,7 @@ Require Import rt.restructuring.model.preemption.task.parameters.
 Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
 Require Import rt.restructuring.model.schedule.work_conserving.
 Require Import rt.restructuring.model.priority.classes.
-Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
+Require Import rt.restructuring.model.schedule.priority_driven.
 Require Import rt.restructuring.analysis.arrival.workload_bound.
 Require Import rt.restructuring.analysis.arrival.rbf.
 Require Export rt.restructuring.analysis.fixed_priority.rta.response_time_bound.
diff --git a/restructuring/analysis/fixed_priority/rta/response_time_bound.v b/restructuring/analysis/fixed_priority/rta/response_time_bound.v
index b1ed59948ef82442590c1d13f562d4e994b2e240..facdb26cd2d81d09bfbcb22aeeb8514e435259fc 100644
--- a/restructuring/analysis/fixed_priority/rta/response_time_bound.v
+++ b/restructuring/analysis/fixed_priority/rta/response_time_bound.v
@@ -13,7 +13,7 @@ Require Import rt.restructuring.model.preemption.task.parameters.
 Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
 Require Import rt.restructuring.model.schedule.work_conserving.
 Require Import rt.restructuring.model.priority.classes.
-Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
+Require Import rt.restructuring.model.schedule.priority_driven.
 Require Import rt.restructuring.analysis.arrival.workload_bound.
 Require Import rt.restructuring.analysis.arrival.rbf.
 Require Export rt.restructuring.analysis.schedulability.
diff --git a/restructuring/model/schedule/priority_based/preemptive.v b/restructuring/model/schedule/priority_based/preemptive.v
deleted file mode 100644
index d41123a36162d9457361287de6f734b8648b4130..0000000000000000000000000000000000000000
--- a/restructuring/model/schedule/priority_based/preemptive.v
+++ /dev/null
@@ -1,28 +0,0 @@
-Require Export rt.restructuring.model.priority.classes.
-
-(** We now define what it means for a schedule to respect a priority *)
-(** We only define it for a JLDP policy since the definitions for JLDP and JLFP are the same
-   and can be used through the conversions *)
-Section Priority.
-  Context {Job: JobType} {Task: TaskType}.
-  Context `{JobCost Job} `{JobArrival Job}.
-
-  Context `{JLDP_policy Job}.
-
-  Variable arr_seq : arrival_sequence Job.
-
-  Context {PState : Type}.
-  Context `{ProcessorState Job PState}.
-
-  Context `{JobReady Job PState}.
-
-  Variable sched : schedule PState.
-
-  Definition respects_preemptive_priorities :=
-    forall j j_hp t,
-      arrives_in arr_seq j ->
-      backlogged sched j t ->
-      scheduled_at sched j_hp t ->
-      hep_job_at t j_hp j.
-  
-End Priority.
diff --git a/restructuring/model/schedule/priority_based/preemption_aware.v b/restructuring/model/schedule/priority_driven.v
similarity index 100%
rename from restructuring/model/schedule/priority_based/preemption_aware.v
rename to restructuring/model/schedule/priority_driven.v