diff --git a/Makefile b/Makefile
index 0fb66166acea05221bdd8ef90493c6ea28192757..5b33988c750365b5877202bcb8df1f79b2dc79a9 100644
--- a/Makefile
+++ b/Makefile
@@ -14,7 +14,7 @@
 
 #
 # This Makefile was generated by the command line :
-# coq_makefile -f _CoqProject ./util/fixedpoint.v ./util/ssromega.v ./util/bigcat.v ./util/nat.v ./util/seqset.v ./util/notation.v ./util/list.v ./util/powerset.v ./util/all.v ./util/sorting.v ./util/tactics.v ./util/bigord.v ./util/induction.v ./util/ord_quantifier.v ./util/sum.v ./util/divround.v ./util/counting.v ./implementation/basic/bertogna_edf_example.v ./implementation/basic/task.v ./implementation/basic/schedule.v ./implementation/basic/bertogna_fp_example.v ./implementation/basic/job.v ./implementation/basic/arrival_sequence.v ./implementation/parallel/bertogna_edf_example.v ./implementation/parallel/task.v ./implementation/parallel/schedule.v ./implementation/parallel/bertogna_fp_example.v ./implementation/parallel/job.v ./implementation/parallel/arrival_sequence.v ./implementation/jitter/bertogna_edf_example.v ./implementation/jitter/task.v ./implementation/jitter/schedule.v ./implementation/jitter/bertogna_fp_example.v ./implementation/jitter/job.v ./implementation/jitter/arrival_sequence.v ./implementation/apa/bertogna_edf_example.v ./implementation/apa/task.v ./implementation/apa/schedule.v ./implementation/apa/bertogna_fp_example.v ./implementation/apa/job.v ./implementation/apa/arrival_sequence.v ./analysis/basic/bertogna_fp_theory.v ./analysis/basic/interference_bound_edf.v ./analysis/basic/interference_bound_fp.v ./analysis/basic/interference_bound.v ./analysis/basic/bertogna_edf_comp.v ./analysis/basic/bertogna_fp_comp.v ./analysis/basic/bertogna_edf_theory.v ./analysis/basic/workload_bound.v ./analysis/parallel/bertogna_fp_theory.v ./analysis/parallel/interference_bound_edf.v ./analysis/parallel/interference_bound_fp.v ./analysis/parallel/interference_bound.v ./analysis/parallel/bertogna_edf_comp.v ./analysis/parallel/bertogna_fp_comp.v ./analysis/parallel/bertogna_edf_theory.v ./analysis/parallel/workload_bound.v ./analysis/jitter/bertogna_fp_theory.v ./analysis/jitter/interference_bound_edf.v ./analysis/jitter/interference_bound_fp.v ./analysis/jitter/interference_bound.v ./analysis/jitter/bertogna_edf_comp.v ./analysis/jitter/bertogna_fp_comp.v ./analysis/jitter/bertogna_edf_theory.v ./analysis/jitter/workload_bound.v ./analysis/apa/bertogna_fp_theory.v ./analysis/apa/interference_bound_edf.v ./analysis/apa/interference_bound_fp.v ./analysis/apa/interference_bound.v ./analysis/apa/bertogna_edf_comp.v ./analysis/apa/bertogna_fp_comp.v ./analysis/apa/bertogna_edf_theory.v ./analysis/apa/workload_bound.v ./model/basic/time.v ./model/basic/schedulability.v ./model/basic/task.v ./model/basic/task_arrival.v ./model/basic/platform.v ./model/basic/schedule.v ./model/basic/priority.v ./model/basic/interference_edf.v ./model/basic/interference.v ./model/basic/constrained_deadlines.v ./model/basic/workload.v ./model/basic/job.v ./model/basic/arrival_sequence.v ./model/basic/response_time.v ./model/jitter/time.v ./model/jitter/schedulability.v ./model/jitter/task.v ./model/jitter/task_arrival.v ./model/jitter/platform.v ./model/jitter/schedule.v ./model/jitter/priority.v ./model/jitter/interference_edf.v ./model/jitter/interference.v ./model/jitter/constrained_deadlines.v ./model/jitter/workload.v ./model/jitter/job.v ./model/jitter/arrival_sequence.v ./model/jitter/response_time.v ./model/apa/time.v ./model/apa/schedulability.v ./model/apa/task.v ./model/apa/task_arrival.v ./model/apa/platform.v ./model/apa/schedule.v ./model/apa/priority.v ./model/apa/affinity.v ./model/apa/interference_edf.v ./model/apa/interference.v ./model/apa/constrained_deadlines.v ./model/apa/workload.v ./model/apa/job.v ./model/apa/arrival_sequence.v ./model/apa/response_time.v -o Makefile 
+# coq_makefile -f _CoqProject ./util/ssromega.v ./util/seqset.v ./util/sorting.v ./util/powerset.v ./util/all.v ./util/ord_quantifier.v ./util/nat.v ./util/sum.v ./util/bigord.v ./util/counting.v ./util/tactics.v ./util/induction.v ./util/list.v ./util/divround.v ./util/bigcat.v ./util/fixedpoint.v ./util/notation.v ./analysis/global/jitter/bertogna_fp_comp.v ./analysis/global/jitter/interference_bound_edf.v ./analysis/global/jitter/workload_bound.v ./analysis/global/jitter/bertogna_edf_comp.v ./analysis/global/jitter/bertogna_fp_theory.v ./analysis/global/jitter/interference_bound.v ./analysis/global/jitter/interference_bound_fp.v ./analysis/global/jitter/bertogna_edf_theory.v ./analysis/global/parallel/bertogna_fp_comp.v ./analysis/global/parallel/interference_bound_edf.v ./analysis/global/parallel/workload_bound.v ./analysis/global/parallel/bertogna_edf_comp.v ./analysis/global/parallel/bertogna_fp_theory.v ./analysis/global/parallel/interference_bound.v ./analysis/global/parallel/interference_bound_fp.v ./analysis/global/parallel/bertogna_edf_theory.v ./analysis/global/basic/bertogna_fp_comp.v ./analysis/global/basic/interference_bound_edf.v ./analysis/global/basic/workload_bound.v ./analysis/global/basic/bertogna_edf_comp.v ./analysis/global/basic/bertogna_fp_theory.v ./analysis/global/basic/interference_bound.v ./analysis/global/basic/interference_bound_fp.v ./analysis/global/basic/bertogna_edf_theory.v ./analysis/apa/bertogna_fp_comp.v ./analysis/apa/interference_bound_edf.v ./analysis/apa/workload_bound.v ./analysis/apa/bertogna_edf_comp.v ./analysis/apa/bertogna_fp_theory.v ./analysis/apa/interference_bound.v ./analysis/apa/interference_bound_fp.v ./analysis/apa/bertogna_edf_theory.v ./model/arrival_sequence.v ./model/task.v ./model/task_arrival.v ./model/priority.v ./model/global/workload.v ./model/global/schedulability.v ./model/global/jitter/interference_edf.v ./model/global/jitter/interference.v ./model/global/jitter/job.v ./model/global/jitter/constrained_deadlines.v ./model/global/jitter/schedule.v ./model/global/jitter/platform.v ./model/global/response_time.v ./model/global/basic/interference_edf.v ./model/global/basic/interference.v ./model/global/basic/constrained_deadlines.v ./model/global/basic/schedule.v ./model/global/basic/platform.v ./model/job.v ./model/time.v ./model/apa/interference_edf.v ./model/apa/interference.v ./model/apa/affinity.v ./model/apa/constrained_deadlines.v ./model/apa/platform.v ./implementation/global/jitter/arrival_sequence.v ./implementation/global/jitter/task.v ./implementation/global/jitter/bertogna_edf_example.v ./implementation/global/jitter/job.v ./implementation/global/jitter/bertogna_fp_example.v ./implementation/global/jitter/schedule.v ./implementation/global/parallel/arrival_sequence.v ./implementation/global/parallel/task.v ./implementation/global/parallel/bertogna_edf_example.v ./implementation/global/parallel/job.v ./implementation/global/parallel/bertogna_fp_example.v ./implementation/global/parallel/schedule.v ./implementation/global/basic/arrival_sequence.v ./implementation/global/basic/task.v ./implementation/global/basic/bertogna_edf_example.v ./implementation/global/basic/job.v ./implementation/global/basic/bertogna_fp_example.v ./implementation/global/basic/schedule.v ./implementation/apa/arrival_sequence.v ./implementation/apa/task.v ./implementation/apa/bertogna_edf_example.v ./implementation/apa/job.v ./implementation/apa/bertogna_fp_example.v ./implementation/apa/schedule.v -o Makefile 
 #
 
 .DEFAULT_GOAL := all
@@ -94,122 +94,104 @@ endif
 #                    #
 ######################
 
-VFILES:=util/fixedpoint.v\
-  util/ssromega.v\
-  util/bigcat.v\
-  util/nat.v\
+VFILES:=util/ssromega.v\
   util/seqset.v\
-  util/notation.v\
-  util/list.v\
+  util/sorting.v\
   util/powerset.v\
   util/all.v\
-  util/sorting.v\
-  util/tactics.v\
-  util/bigord.v\
-  util/induction.v\
   util/ord_quantifier.v\
+  util/nat.v\
   util/sum.v\
-  util/divround.v\
+  util/bigord.v\
   util/counting.v\
-  implementation/basic/bertogna_edf_example.v\
-  implementation/basic/task.v\
-  implementation/basic/schedule.v\
-  implementation/basic/bertogna_fp_example.v\
-  implementation/basic/job.v\
-  implementation/basic/arrival_sequence.v\
-  implementation/parallel/bertogna_edf_example.v\
-  implementation/parallel/task.v\
-  implementation/parallel/schedule.v\
-  implementation/parallel/bertogna_fp_example.v\
-  implementation/parallel/job.v\
-  implementation/parallel/arrival_sequence.v\
-  implementation/jitter/bertogna_edf_example.v\
-  implementation/jitter/task.v\
-  implementation/jitter/schedule.v\
-  implementation/jitter/bertogna_fp_example.v\
-  implementation/jitter/job.v\
-  implementation/jitter/arrival_sequence.v\
-  implementation/apa/bertogna_edf_example.v\
-  implementation/apa/task.v\
-  implementation/apa/schedule.v\
-  implementation/apa/bertogna_fp_example.v\
-  implementation/apa/job.v\
-  implementation/apa/arrival_sequence.v\
-  analysis/basic/bertogna_fp_theory.v\
-  analysis/basic/interference_bound_edf.v\
-  analysis/basic/interference_bound_fp.v\
-  analysis/basic/interference_bound.v\
-  analysis/basic/bertogna_edf_comp.v\
-  analysis/basic/bertogna_fp_comp.v\
-  analysis/basic/bertogna_edf_theory.v\
-  analysis/basic/workload_bound.v\
-  analysis/parallel/bertogna_fp_theory.v\
-  analysis/parallel/interference_bound_edf.v\
-  analysis/parallel/interference_bound_fp.v\
-  analysis/parallel/interference_bound.v\
-  analysis/parallel/bertogna_edf_comp.v\
-  analysis/parallel/bertogna_fp_comp.v\
-  analysis/parallel/bertogna_edf_theory.v\
-  analysis/parallel/workload_bound.v\
-  analysis/jitter/bertogna_fp_theory.v\
-  analysis/jitter/interference_bound_edf.v\
-  analysis/jitter/interference_bound_fp.v\
-  analysis/jitter/interference_bound.v\
-  analysis/jitter/bertogna_edf_comp.v\
-  analysis/jitter/bertogna_fp_comp.v\
-  analysis/jitter/bertogna_edf_theory.v\
-  analysis/jitter/workload_bound.v\
-  analysis/apa/bertogna_fp_theory.v\
+  util/tactics.v\
+  util/induction.v\
+  util/list.v\
+  util/divround.v\
+  util/bigcat.v\
+  util/fixedpoint.v\
+  util/notation.v\
+  analysis/global/jitter/bertogna_fp_comp.v\
+  analysis/global/jitter/interference_bound_edf.v\
+  analysis/global/jitter/workload_bound.v\
+  analysis/global/jitter/bertogna_edf_comp.v\
+  analysis/global/jitter/bertogna_fp_theory.v\
+  analysis/global/jitter/interference_bound.v\
+  analysis/global/jitter/interference_bound_fp.v\
+  analysis/global/jitter/bertogna_edf_theory.v\
+  analysis/global/parallel/bertogna_fp_comp.v\
+  analysis/global/parallel/interference_bound_edf.v\
+  analysis/global/parallel/workload_bound.v\
+  analysis/global/parallel/bertogna_edf_comp.v\
+  analysis/global/parallel/bertogna_fp_theory.v\
+  analysis/global/parallel/interference_bound.v\
+  analysis/global/parallel/interference_bound_fp.v\
+  analysis/global/parallel/bertogna_edf_theory.v\
+  analysis/global/basic/bertogna_fp_comp.v\
+  analysis/global/basic/interference_bound_edf.v\
+  analysis/global/basic/workload_bound.v\
+  analysis/global/basic/bertogna_edf_comp.v\
+  analysis/global/basic/bertogna_fp_theory.v\
+  analysis/global/basic/interference_bound.v\
+  analysis/global/basic/interference_bound_fp.v\
+  analysis/global/basic/bertogna_edf_theory.v\
+  analysis/apa/bertogna_fp_comp.v\
   analysis/apa/interference_bound_edf.v\
-  analysis/apa/interference_bound_fp.v\
-  analysis/apa/interference_bound.v\
+  analysis/apa/workload_bound.v\
   analysis/apa/bertogna_edf_comp.v\
-  analysis/apa/bertogna_fp_comp.v\
+  analysis/apa/bertogna_fp_theory.v\
+  analysis/apa/interference_bound.v\
+  analysis/apa/interference_bound_fp.v\
   analysis/apa/bertogna_edf_theory.v\
-  analysis/apa/workload_bound.v\
-  model/basic/time.v\
-  model/basic/schedulability.v\
-  model/basic/task.v\
-  model/basic/task_arrival.v\
-  model/basic/platform.v\
-  model/basic/schedule.v\
-  model/basic/priority.v\
-  model/basic/interference_edf.v\
-  model/basic/interference.v\
-  model/basic/constrained_deadlines.v\
-  model/basic/workload.v\
-  model/basic/job.v\
-  model/basic/arrival_sequence.v\
-  model/basic/response_time.v\
-  model/jitter/time.v\
-  model/jitter/schedulability.v\
-  model/jitter/task.v\
-  model/jitter/task_arrival.v\
-  model/jitter/platform.v\
-  model/jitter/schedule.v\
-  model/jitter/priority.v\
-  model/jitter/interference_edf.v\
-  model/jitter/interference.v\
-  model/jitter/constrained_deadlines.v\
-  model/jitter/workload.v\
-  model/jitter/job.v\
-  model/jitter/arrival_sequence.v\
-  model/jitter/response_time.v\
-  model/apa/time.v\
-  model/apa/schedulability.v\
-  model/apa/task.v\
-  model/apa/task_arrival.v\
-  model/apa/platform.v\
-  model/apa/schedule.v\
-  model/apa/priority.v\
-  model/apa/affinity.v\
+  model/arrival_sequence.v\
+  model/task.v\
+  model/task_arrival.v\
+  model/priority.v\
+  model/global/workload.v\
+  model/global/schedulability.v\
+  model/global/jitter/interference_edf.v\
+  model/global/jitter/interference.v\
+  model/global/jitter/job.v\
+  model/global/jitter/constrained_deadlines.v\
+  model/global/jitter/schedule.v\
+  model/global/jitter/platform.v\
+  model/global/response_time.v\
+  model/global/basic/interference_edf.v\
+  model/global/basic/interference.v\
+  model/global/basic/constrained_deadlines.v\
+  model/global/basic/schedule.v\
+  model/global/basic/platform.v\
+  model/job.v\
+  model/time.v\
   model/apa/interference_edf.v\
   model/apa/interference.v\
+  model/apa/affinity.v\
   model/apa/constrained_deadlines.v\
-  model/apa/workload.v\
-  model/apa/job.v\
-  model/apa/arrival_sequence.v\
-  model/apa/response_time.v
+  model/apa/platform.v\
+  implementation/global/jitter/arrival_sequence.v\
+  implementation/global/jitter/task.v\
+  implementation/global/jitter/bertogna_edf_example.v\
+  implementation/global/jitter/job.v\
+  implementation/global/jitter/bertogna_fp_example.v\
+  implementation/global/jitter/schedule.v\
+  implementation/global/parallel/arrival_sequence.v\
+  implementation/global/parallel/task.v\
+  implementation/global/parallel/bertogna_edf_example.v\
+  implementation/global/parallel/job.v\
+  implementation/global/parallel/bertogna_fp_example.v\
+  implementation/global/parallel/schedule.v\
+  implementation/global/basic/arrival_sequence.v\
+  implementation/global/basic/task.v\
+  implementation/global/basic/bertogna_edf_example.v\
+  implementation/global/basic/job.v\
+  implementation/global/basic/bertogna_fp_example.v\
+  implementation/global/basic/schedule.v\
+  implementation/apa/arrival_sequence.v\
+  implementation/apa/task.v\
+  implementation/apa/bertogna_edf_example.v\
+  implementation/apa/job.v\
+  implementation/apa/bertogna_fp_example.v\
+  implementation/apa/schedule.v
 
 ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),)
 -include $(addsuffix .d,$(VFILES))
diff --git a/README.md b/README.md
index 11e94337504550e42abb498c8758bf52d2dc7c21..8d5003a12e6ae0db5048d9d36465ac279adfb295 100644
--- a/README.md
+++ b/README.md
@@ -2,17 +2,39 @@
 
 This repository contains the main Coq proof spec & proof development of the RT-PROOFS project.
 
+## Directory Structure
 
-## Plan
+The Prosa directory is organized in a hierarchy: while generic, reusable foundations stay in
+the upper levels, definitions for specific analyses should go deeper into the directory tree.
 
-For now, this is more or less just a "code dump" with a flat hierarchy to get things started.
+### Base Directories
 
-Going forward, the goal is to both
+Currently, Prosa contains the following base directories:
 
-- restructure the repository as it grows in scope, and to
+- **model/:** Specification of task and scheduler models, as well as generic lemmas related to scheduling.
+	  
+- **analysis/:** Definition, proofs and implementation of schedulability analyses.
 
-- add significant documentation to make it easier to bring new collaborators who are not yet familiar with Coq into the project.
+- **implementation/:** Instantiation of each schedulability analysis with concrete task and scheduler implementations.
+		       Testing the main theorems in an assumption free environment shows the absence of contradictions.
 
+### Internal Directories
+
+Within each base directory you can find the different classes of schedulers.
+
+- **model/uni:** Uniprocessor scheduling.
+- **model/global:** Global scheduling.
+- **model/partitioned:** Partitioned scheduling.
+- **model/apa:** APA scheduling.
+
+### Extending Prosa
+
+When adding a new model or analysis to Prosa, please extend the corresponding directory.
+For example, the schedulability analysis for global scheduling with release jitter is organized as follows.
+
+- **model/global/jitter:** Definitions and lemmas for global scheduling with release jitter.
+- **analysis/global/jitter:** Analysis for global scheduling with release jitter.
+- **implementation/global/jitter:** Implementation of the concrete scheduler with release jitter. 
 
 ## Commit and Development Rules
 
@@ -26,4 +48,6 @@ Going forward, the goal is to both
 
 5. Pushing fixes, small improvements, etc. is always ok. 
 
-6. Document the tactics that you use in the [list of tactics](doc/tactics.md).
\ No newline at end of file
+6. Document the tactics that you use in the [list of tactics](doc/tactics.md).
+
+7. Whenever you have time available, please help with extending the documentation. :-)
\ No newline at end of file
diff --git a/analysis/apa/bertogna_edf_theory.v b/analysis/apa/bertogna_edf_theory.v
index 97485a09c0f93da117bdc49457d5bbe50c75f7da..096c3e8e741b0be13f9369cd1ca7fb768dd51e23 100644
--- a/analysis/apa/bertogna_edf_theory.v
+++ b/analysis/apa/bertogna_edf_theory.v
@@ -1,8 +1,9 @@
 Require Import rt.util.all rt.util.divround.
-Require Import rt.model.apa.task rt.model.apa.job rt.model.apa.task_arrival
-               rt.model.apa.schedule rt.model.apa.platform rt.model.apa.interference
-               rt.model.apa.workload rt.model.apa.schedulability rt.model.apa.priority
-               rt.model.apa.platform rt.model.apa.response_time
+Require Import rt.model.task rt.model.job rt.model.priority rt.model.task_arrival.
+Require Import rt.model.global.workload rt.model.global.response_time
+               rt.model.global.schedulability.
+Require Import rt.model.global.basic.schedule.
+Require Import rt.model.apa.platform rt.model.apa.interference
                rt.model.apa.affinity rt.model.apa.constrained_deadlines.
 Require Import rt.analysis.apa.workload_bound rt.analysis.apa.interference_bound_edf.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
diff --git a/analysis/apa/bertogna_fp_theory.v b/analysis/apa/bertogna_fp_theory.v
index f3a912c844fa513c580e84e114c4ecb1c3f175bc..4c25c5e3c54e1562b38969d2c0dee086f529c9f5 100644
--- a/analysis/apa/bertogna_fp_theory.v
+++ b/analysis/apa/bertogna_fp_theory.v
@@ -1,10 +1,12 @@
-Require Import rt.util.all rt.util.divround.
-Require Import rt.model.apa.task rt.model.apa.job rt.model.apa.task_arrival
-               rt.model.apa.schedule rt.model.apa.platform rt.model.apa.constrained_deadlines
-               rt.model.apa.workload rt.model.apa.schedulability rt.model.apa.priority
-               rt.model.apa.response_time rt.model.apa.interference
-               rt.model.apa.affinity rt.model.apa.constrained_deadlines.
-Require Import rt.analysis.apa.workload_bound rt.analysis.apa.interference_bound_fp.
+Require Import rt.util.all.
+Require Import rt.model.task rt.model.job rt.model.priority rt.model.task_arrival.
+Require Import rt.model.global.response_time rt.model.global.schedulability
+               rt.model.global.workload.
+Require Import rt.model.global.basic.schedule.
+Require Import rt.model.apa.platform rt.model.apa.constrained_deadlines
+               rt.model.apa.interference rt.model.apa.affinity.
+Require Import rt.analysis.apa.workload_bound
+               rt.analysis.apa.interference_bound_fp.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
 
 Module ResponseTimeAnalysisFP.
@@ -13,7 +15,6 @@ Module ResponseTimeAnalysisFP.
          Platform Schedulability ResponseTime Priority
          SporadicTaskArrival WorkloadBound Affinity ConstrainedDeadlines.
     
-
   (* In this section, we prove that any fixed point in the APA-reduction of Bertogna
      and Cirinei's RTA for FP scheduling with slack updates is a safe response-time
      bound. This result corresponds to Lemma 9 in the revised version of the APA paper:
diff --git a/analysis/apa/interference_bound.v b/analysis/apa/interference_bound.v
index 8814c15fd5e5d9dca4d056c30f5488799e982c9c..a3971721f6b0a790c9c4d929dcae695e2777a6a2 100644
--- a/analysis/apa/interference_bound.v
+++ b/analysis/apa/interference_bound.v
@@ -1,5 +1,5 @@
 Require Import rt.util.all.
-Require Import rt.model.apa.schedule.
+Require Import rt.model.global.basic.schedule.
 Require Import rt.analysis.apa.workload_bound.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
diff --git a/analysis/apa/interference_bound_edf.v b/analysis/apa/interference_bound_edf.v
index ef241c8cca672c9b6c2af616e541b3ce1f87fe01..f3496782284cb76ee14185d9086c79572442d3dc 100644
--- a/analysis/apa/interference_bound_edf.v
+++ b/analysis/apa/interference_bound_edf.v
@@ -1,9 +1,10 @@
 Require Import rt.util.all rt.util.divround.
-Require Import rt.model.apa.task rt.model.apa.job rt.model.apa.schedule
-               rt.model.apa.task_arrival rt.model.apa.platform rt.model.apa.response_time
-               rt.model.apa.workload rt.model.apa.priority rt.model.apa.schedulability
-               rt.model.apa.interference rt.model.apa.interference_edf
-               rt.model.apa.affinity.
+Require Import rt.model.job rt.model.task rt.model.priority rt.model.task_arrival.
+Require Import rt.model.global.workload rt.model.global.response_time
+               rt.model.global.schedulability.
+Require Import rt.model.global.basic.schedule.
+Require Import rt.model.apa.platform rt.model.apa.interference
+               rt.model.apa.interference_edf rt.model.apa.affinity.
 Require Import rt.analysis.apa.workload_bound rt.analysis.apa.interference_bound.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
 
diff --git a/analysis/apa/interference_bound_fp.v b/analysis/apa/interference_bound_fp.v
index 54230846186d9fd11aaf14029edb2501f362bea9..b23243a59111a8a5f8a9618a32fbb9e18ff18b44 100644
--- a/analysis/apa/interference_bound_fp.v
+++ b/analysis/apa/interference_bound_fp.v
@@ -1,6 +1,8 @@
 Require Import rt.util.all.
-Require Import rt.model.apa.schedule rt.model.apa.priority rt.model.apa.workload
-               rt.model.apa.interference rt.model.apa.affinity.
+Require Import rt.model.priority.
+Require Import rt.model.global.workload.
+Require Import rt.model.global.basic.schedule.
+Require Import rt.model.apa.interference rt.model.apa.affinity.
 Require Import rt.analysis.apa.workload_bound rt.analysis.apa.interference_bound.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
diff --git a/analysis/apa/workload_bound.v b/analysis/apa/workload_bound.v
index ce0b848479f04163405b6e5751e1c1f922ac86d2..1d9a4c86987ae8a71d60fcd7b750b73e9fa1e3dc 100644
--- a/analysis/apa/workload_bound.v
+++ b/analysis/apa/workload_bound.v
@@ -1,7 +1,8 @@
 Require Import rt.util.all rt.util.divround.
-Require Import rt.model.apa.task rt.model.apa.job rt.model.apa.schedule
-               rt.model.apa.task_arrival rt.model.apa.response_time
-               rt.model.apa.workload rt.model.apa.schedulability.
+Require Import rt.model.task rt.model.job rt.model.task_arrival.
+Require Import rt.model.global.response_time rt.model.global.schedulability
+               rt.model.global.workload.
+Require Import rt.model.global.basic.schedule.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq div fintype bigop path.
 
 Module WorkloadBound.
diff --git a/analysis/basic/bertogna_edf_comp.v b/analysis/global/basic/bertogna_edf_comp.v
similarity index 99%
rename from analysis/basic/bertogna_edf_comp.v
rename to analysis/global/basic/bertogna_edf_comp.v
index 3bc47989a57b84f8797162319c04d987e83d07b0..ad6f43082fa69e2771be297eab07409f7f3a23d8 100755
--- a/analysis/basic/bertogna_edf_comp.v
+++ b/analysis/global/basic/bertogna_edf_comp.v
@@ -1,5 +1,5 @@
 Require Import rt.util.all.
-Require Import rt.analysis.basic.bertogna_edf_theory.
+Require Import rt.analysis.global.basic.bertogna_edf_theory.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
 
 Module ResponseTimeIterationEDF.
diff --git a/analysis/basic/bertogna_edf_theory.v b/analysis/global/basic/bertogna_edf_theory.v
similarity index 98%
rename from analysis/basic/bertogna_edf_theory.v
rename to analysis/global/basic/bertogna_edf_theory.v
index b35dc603940d33bdebdcc6f9bec7e8859002c4d9..8b01b6f746aea301a9496c1a8d9f77ab62663a52 100644
--- a/analysis/basic/bertogna_edf_theory.v
+++ b/analysis/global/basic/bertogna_edf_theory.v
@@ -1,10 +1,11 @@
 Require Import rt.util.all.
-Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.task_arrival
-               rt.model.basic.schedule rt.model.basic.platform rt.model.basic.interference
-               rt.model.basic.workload rt.model.basic.schedulability rt.model.basic.priority
-               rt.model.basic.platform rt.model.basic.response_time
-               rt.model.basic.constrained_deadlines.
-Require Import rt.analysis.basic.workload_bound rt.analysis.basic.interference_bound_edf.
+Require Import rt.model.task rt.model.job rt.model.task_arrival rt.model.priority.
+Require Import rt.model.global.workload rt.model.global.schedulability
+               rt.model.global.response_time.
+Require Import rt.model.global.basic.schedule rt.model.global.basic.platform
+               rt.model.global.basic.interference rt.model.global.basic.platform
+               rt.model.global.basic.constrained_deadlines.
+Require Import rt.analysis.global.basic.workload_bound rt.analysis.global.basic.interference_bound_edf.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
 
 Module ResponseTimeAnalysisEDF.
diff --git a/analysis/basic/bertogna_fp_comp.v b/analysis/global/basic/bertogna_fp_comp.v
similarity index 99%
rename from analysis/basic/bertogna_fp_comp.v
rename to analysis/global/basic/bertogna_fp_comp.v
index 7208a9ee6eb20055852dc3077187d9a6f66444c1..6bc0e4d64a00e1b4eb14ce8d09339a89418f87d4 100644
--- a/analysis/basic/bertogna_fp_comp.v
+++ b/analysis/global/basic/bertogna_fp_comp.v
@@ -1,5 +1,5 @@
 Require Import rt.util.all.
-Require Import rt.analysis.basic.bertogna_fp_theory.
+Require Import rt.analysis.global.basic.bertogna_fp_theory.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop div path.
 
 Module ResponseTimeIterationFP.
diff --git a/analysis/basic/bertogna_fp_theory.v b/analysis/global/basic/bertogna_fp_theory.v
similarity index 98%
rename from analysis/basic/bertogna_fp_theory.v
rename to analysis/global/basic/bertogna_fp_theory.v
index 637f1f5f439908a43e8cdfa9150dc698fc5022d9..2df63d4f1eeb204d879da2085992a358a55392c5 100644
--- a/analysis/basic/bertogna_fp_theory.v
+++ b/analysis/global/basic/bertogna_fp_theory.v
@@ -1,9 +1,11 @@
 Require Import rt.util.all.
-Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.task_arrival
-               rt.model.basic.schedule rt.model.basic.platform rt.model.basic.constrained_deadlines
-               rt.model.basic.workload rt.model.basic.schedulability rt.model.basic.priority
-               rt.model.basic.response_time rt.model.basic.interference.
-Require Import rt.analysis.basic.workload_bound rt.analysis.basic.interference_bound_fp.
+Require Import rt.model.task rt.model.job rt.model.priority rt.model.task_arrival.
+Require Import rt.model.global.workload rt.model.global.schedulability
+               rt.model.global.response_time.
+Require Import rt.model.global.basic.schedule rt.model.global.basic.platform
+               rt.model.global.basic.constrained_deadlines rt.model.global.basic.interference.
+Require Import rt.analysis.global.basic.workload_bound
+               rt.analysis.global.basic.interference_bound_fp.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
 
 Module ResponseTimeAnalysisFP.
diff --git a/analysis/basic/interference_bound.v b/analysis/global/basic/interference_bound.v
similarity index 92%
rename from analysis/basic/interference_bound.v
rename to analysis/global/basic/interference_bound.v
index c5ecc342dd9afda68f7867f69427e01361fe2b7a..8edaa74f4d5d4de3d0e2ab8b63889d1315e065e0 100644
--- a/analysis/basic/interference_bound.v
+++ b/analysis/global/basic/interference_bound.v
@@ -1,6 +1,6 @@
 Require Import rt.util.all.
-Require Import rt.model.basic.schedule.
-Require Import rt.analysis.basic.workload_bound.
+Require Import rt.model.global.basic.schedule.
+Require Import rt.analysis.global.basic.workload_bound.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 Module InterferenceBoundGeneric.
diff --git a/analysis/basic/interference_bound_edf.v b/analysis/global/basic/interference_bound_edf.v
similarity index 99%
rename from analysis/basic/interference_bound_edf.v
rename to analysis/global/basic/interference_bound_edf.v
index 592123f1bd3cd522916db50e814be9bada0dd6d6..d2f67484720fff10ff1d7ba555c3f917be20a6e6 100644
--- a/analysis/basic/interference_bound_edf.v
+++ b/analysis/global/basic/interference_bound_edf.v
@@ -1,9 +1,11 @@
 Require Import rt.util.all.
-Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.schedule
-               rt.model.basic.task_arrival rt.model.basic.platform rt.model.basic.response_time
-               rt.model.basic.workload rt.model.basic.priority rt.model.basic.schedulability
-               rt.model.basic.interference rt.model.basic.interference_edf.
-Require Import rt.analysis.basic.workload_bound rt.analysis.basic.interference_bound.
+Require Import rt.model.task rt.model.job rt.model.task_arrival rt.model.priority.
+Require Import rt.model.global.response_time rt.model.global.workload
+               rt.model.global.schedulability.
+Require Import rt.model.global.basic.schedule rt.model.global.basic.platform
+               rt.model.global.basic.interference rt.model.global.basic.interference_edf.
+Require Import rt.analysis.global.basic.workload_bound
+               rt.analysis.global.basic.interference_bound.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
 
 Module InterferenceBoundEDF.
diff --git a/analysis/basic/interference_bound_fp.v b/analysis/global/basic/interference_bound_fp.v
similarity index 83%
rename from analysis/basic/interference_bound_fp.v
rename to analysis/global/basic/interference_bound_fp.v
index da6ad7ca34fc537a69ef91aee025f042dd375dfd..8f35377425e7336829000a5d42645047bfb91f38 100644
--- a/analysis/basic/interference_bound_fp.v
+++ b/analysis/global/basic/interference_bound_fp.v
@@ -1,7 +1,9 @@
 Require Import rt.util.all.
-Require Import rt.model.basic.schedule rt.model.basic.priority rt.model.basic.workload
-               rt.model.basic.interference.
-Require Import rt.analysis.basic.workload_bound rt.analysis.basic.interference_bound.
+Require Import rt.model.priority.
+Require Import rt.model.global.workload.
+Require Import rt.model.global.basic.schedule rt.model.global.basic.interference.
+Require Import rt.analysis.global.basic.workload_bound
+               rt.analysis.global.basic.interference_bound.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 Module InterferenceBoundFP.
diff --git a/analysis/basic/workload_bound.v b/analysis/global/basic/workload_bound.v
similarity index 99%
rename from analysis/basic/workload_bound.v
rename to analysis/global/basic/workload_bound.v
index 70b0436acfbbfd5e0a2cce2a5215bce47f6648f4..f086c910483de4e1cc6d3f14141a925f2f025893 100644
--- a/analysis/basic/workload_bound.v
+++ b/analysis/global/basic/workload_bound.v
@@ -1,7 +1,8 @@
 Require Import rt.util.all.
-Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.schedule
-               rt.model.basic.task_arrival rt.model.basic.response_time
-               rt.model.basic.workload rt.model.basic.schedulability.
+Require Import rt.model.task rt.model.job rt.model.task_arrival.
+Require Import rt.model.global.workload rt.model.global.response_time
+               rt.model.global.schedulability.
+Require Import rt.model.global.basic.schedule.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq div fintype bigop path.
 
 Module WorkloadBound.
diff --git a/analysis/jitter/bertogna_edf_comp.v b/analysis/global/jitter/bertogna_edf_comp.v
similarity index 99%
rename from analysis/jitter/bertogna_edf_comp.v
rename to analysis/global/jitter/bertogna_edf_comp.v
index 980b598fff516ba93779aaad4352e4660d6ac5b6..31701e5aa13fb812d3726cea523851099a466085 100755
--- a/analysis/jitter/bertogna_edf_comp.v
+++ b/analysis/global/jitter/bertogna_edf_comp.v
@@ -1,5 +1,5 @@
 Require Import rt.util.all.
-Require Import rt.analysis.jitter.bertogna_edf_theory.
+Require Import rt.analysis.global.jitter.bertogna_edf_theory.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
 
 Module ResponseTimeIterationEDF.
diff --git a/analysis/jitter/bertogna_edf_theory.v b/analysis/global/jitter/bertogna_edf_theory.v
similarity index 98%
rename from analysis/jitter/bertogna_edf_theory.v
rename to analysis/global/jitter/bertogna_edf_theory.v
index 71cd4dcba4cbb3a05da10d4da714c77c51518cb1..96112a0540cbe4fdd36869d558f9c193d4479d5d 100644
--- a/analysis/jitter/bertogna_edf_theory.v
+++ b/analysis/global/jitter/bertogna_edf_theory.v
@@ -1,11 +1,12 @@
 Require Import rt.util.all.
-Require Import rt.model.jitter.job rt.model.jitter.task rt.model.jitter.task_arrival
-               rt.model.jitter.schedule rt.model.jitter.platform rt.model.jitter.interference
-               rt.model.jitter.workload rt.model.jitter.schedulability
-               rt.model.jitter.priority rt.model.jitter.constrained_deadlines
-               rt.model.jitter.response_time.
-Require Import rt.analysis.jitter.workload_bound
-               rt.analysis.jitter.interference_bound_edf.
+Require Import rt.model.task rt.model.priority rt.model.task_arrival.
+Require Import rt.model.global.workload rt.model.global.schedulability
+               rt.model.global.response_time.
+Require Import rt.model.global.jitter.job rt.model.global.jitter.schedule
+               rt.model.global.jitter.platform rt.model.global.jitter.interference
+               rt.model.global.jitter.constrained_deadlines.
+Require Import rt.analysis.global.jitter.workload_bound
+               rt.analysis.global.jitter.interference_bound_edf.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
 
 Module ResponseTimeAnalysisEDFJitter.
diff --git a/analysis/jitter/bertogna_fp_comp.v b/analysis/global/jitter/bertogna_fp_comp.v
similarity index 99%
rename from analysis/jitter/bertogna_fp_comp.v
rename to analysis/global/jitter/bertogna_fp_comp.v
index 5e9f582142411085eaf419f82baa151677be2504..13b5b83f530ea19bdd0937f5401b2390089e56ed 100644
--- a/analysis/jitter/bertogna_fp_comp.v
+++ b/analysis/global/jitter/bertogna_fp_comp.v
@@ -1,5 +1,5 @@
 Require Import rt.util.all.
-Require Import rt.analysis.jitter.bertogna_fp_theory.
+Require Import rt.analysis.global.jitter.bertogna_fp_theory.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop div path.
 
 Module ResponseTimeIterationFP.
diff --git a/analysis/jitter/bertogna_fp_theory.v b/analysis/global/jitter/bertogna_fp_theory.v
similarity index 98%
rename from analysis/jitter/bertogna_fp_theory.v
rename to analysis/global/jitter/bertogna_fp_theory.v
index c4abdd9bc1d3909530b85f9cd3a8c881f90c7bb0..d9f5cf95647bb40e9548d1da19f56c863a6fb54c 100644
--- a/analysis/jitter/bertogna_fp_theory.v
+++ b/analysis/global/jitter/bertogna_fp_theory.v
@@ -1,9 +1,12 @@
 Require Import rt.util.all.
-Require Import rt.model.jitter.task rt.model.jitter.job rt.model.jitter.task_arrival
-               rt.model.jitter.schedule rt.model.jitter.platform rt.model.jitter.constrained_deadlines
-               rt.model.jitter.workload rt.model.jitter.schedulability rt.model.jitter.priority
-               rt.model.jitter.response_time rt.model.jitter.interference.
-Require Import rt.analysis.jitter.workload_bound rt.analysis.jitter.interference_bound_fp.
+Require Import rt.model.task rt.model.priority rt.model.task_arrival.
+Require Import rt.model.global.workload rt.model.global.response_time
+               rt.model.global.schedulability.
+Require Import rt.model.global.jitter.job rt.model.global.jitter.interference
+               rt.model.global.jitter.schedule rt.model.global.jitter.platform
+               rt.model.global.jitter.constrained_deadlines.
+Require Import rt.analysis.global.jitter.workload_bound
+               rt.analysis.global.jitter.interference_bound_fp.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
 
 Module ResponseTimeAnalysisFP.
diff --git a/analysis/jitter/interference_bound.v b/analysis/global/jitter/interference_bound.v
similarity index 86%
rename from analysis/jitter/interference_bound.v
rename to analysis/global/jitter/interference_bound.v
index 27b9de55059802e7fd10eea81bf09e074bcffe88..d91cdc9a97355ee6fe495d3359dfd08420ca20af 100644
--- a/analysis/jitter/interference_bound.v
+++ b/analysis/global/jitter/interference_bound.v
@@ -1,7 +1,7 @@
 Require Import rt.util.all.
-Require Import rt.model.jitter.arrival_sequence rt.model.jitter.schedule
-               rt.model.jitter.interference rt.model.jitter.priority.
-Require Import rt.analysis.jitter.workload_bound.
+Require Import rt.model.arrival_sequence rt.model.priority.
+Require Import rt.model.global.jitter.schedule rt.model.global.jitter.interference.
+Require Import rt.analysis.global.jitter.workload_bound.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 Module InterferenceBoundJitter.
diff --git a/analysis/jitter/interference_bound_edf.v b/analysis/global/jitter/interference_bound_edf.v
similarity index 99%
rename from analysis/jitter/interference_bound_edf.v
rename to analysis/global/jitter/interference_bound_edf.v
index 48d2fad71370a668c0d5f934aabd1de925dc3eb7..65e0820f80e3bfc2b764eeb38399a35ba3ae608c 100644
--- a/analysis/jitter/interference_bound_edf.v
+++ b/analysis/global/jitter/interference_bound_edf.v
@@ -1,9 +1,11 @@
 Require Import rt.util.all.
-Require Import rt.model.jitter.job rt.model.jitter.task rt.model.jitter.task_arrival
-               rt.model.jitter.schedule rt.model.jitter.platform rt.model.jitter.response_time
-               rt.model.jitter.priority rt.model.jitter.workload rt.model.jitter.schedulability
-               rt.model.jitter.interference rt.model.jitter.interference_edf.
-Require Import rt.analysis.jitter.workload_bound rt.analysis.jitter.interference_bound.
+Require Import rt.model.task rt.model.priority rt.model.task_arrival.
+Require Import rt.model.global.response_time rt.model.global.workload
+               rt.model.global.schedulability.
+Require Import rt.model.global.jitter.job rt.model.global.jitter.schedule
+               rt.model.global.jitter.platform rt.model.global.jitter.interference
+               rt.model.global.jitter.interference_edf.
+Require Import rt.analysis.global.jitter.workload_bound rt.analysis.global.jitter.interference_bound.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
 
 Module InterferenceBoundEDFJitter.
diff --git a/analysis/jitter/interference_bound_fp.v b/analysis/global/jitter/interference_bound_fp.v
similarity index 84%
rename from analysis/jitter/interference_bound_fp.v
rename to analysis/global/jitter/interference_bound_fp.v
index 4bc8c267e84e228ea1d77d49a915c0f3f39fea19..3167a62b1584d7d835342bdbcc9eee347aef03fd 100644
--- a/analysis/jitter/interference_bound_fp.v
+++ b/analysis/global/jitter/interference_bound_fp.v
@@ -1,7 +1,8 @@
 Require Import rt.util.all.
-Require Import rt.model.jitter.schedule rt.model.jitter.priority rt.model.jitter.workload
-               rt.model.jitter.interference.
-Require Import rt.analysis.jitter.workload_bound rt.analysis.jitter.interference_bound.
+Require Import rt.model.priority.
+Require Import rt.model.global.workload.
+Require Import rt.model.global.jitter.schedule rt.model.global.jitter.interference.
+Require Import rt.analysis.global.jitter.workload_bound rt.analysis.global.jitter.interference_bound.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 Module InterferenceBoundFP.
diff --git a/analysis/jitter/workload_bound.v b/analysis/global/jitter/workload_bound.v
similarity index 99%
rename from analysis/jitter/workload_bound.v
rename to analysis/global/jitter/workload_bound.v
index 66bf9677b1cb382d3152e7e00c5f437cbd2b51e8..e12fbd2e6806b526bdf803a64103142f9135eac6 100644
--- a/analysis/jitter/workload_bound.v
+++ b/analysis/global/jitter/workload_bound.v
@@ -1,7 +1,8 @@
 Require Import rt.util.all.
-Require Import rt.model.jitter.task rt.model.jitter.job rt.model.jitter.schedule
-               rt.model.jitter.task_arrival rt.model.jitter.response_time
-               rt.model.jitter.schedulability rt.model.jitter.workload.
+Require Import rt.model.task rt.model.task_arrival.
+Require Import rt.model.global.workload rt.model.global.response_time
+               rt.model.global.schedulability.
+Require Import rt.model.global.jitter.job rt.model.global.jitter.schedule.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq div fintype bigop path.
 
 Module WorkloadBoundJitter.
diff --git a/analysis/parallel/bertogna_edf_comp.v b/analysis/global/parallel/bertogna_edf_comp.v
similarity index 99%
rename from analysis/parallel/bertogna_edf_comp.v
rename to analysis/global/parallel/bertogna_edf_comp.v
index 5ec5b9b7093024e9150231ac0ed5cb1ef6532e0b..32c5f7898fb85b96a1802068c40e29c7fbefa8e2 100755
--- a/analysis/parallel/bertogna_edf_comp.v
+++ b/analysis/global/parallel/bertogna_edf_comp.v
@@ -1,5 +1,5 @@
 Require Import rt.util.all.
-Require Import rt.analysis.parallel.bertogna_edf_theory.
+Require Import rt.analysis.global.parallel.bertogna_edf_theory.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
 
 Module ResponseTimeIterationEDF.
diff --git a/analysis/parallel/bertogna_edf_theory.v b/analysis/global/parallel/bertogna_edf_theory.v
similarity index 98%
rename from analysis/parallel/bertogna_edf_theory.v
rename to analysis/global/parallel/bertogna_edf_theory.v
index 3a7fafdff6f5523cc9b2b722d580ea1579bfb7e1..0e939a9575f97e088d02fc11ba5a61eb8fa224fe 100644
--- a/analysis/parallel/bertogna_edf_theory.v
+++ b/analysis/global/parallel/bertogna_edf_theory.v
@@ -1,9 +1,11 @@
 Require Import rt.util.all.
-Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.task_arrival
-               rt.model.basic.schedule rt.model.basic.platform rt.model.basic.interference
-               rt.model.basic.workload rt.model.basic.schedulability rt.model.basic.priority
-               rt.model.basic.platform rt.model.basic.response_time.
-Require Import rt.analysis.parallel.workload_bound rt.analysis.parallel.interference_bound_edf.
+Require Import rt.model.task rt.model.job rt.model.task_arrival rt.model.priority.
+Require Import rt.model.global.workload rt.model.global.schedulability
+               rt.model.global.response_time.
+Require Import rt.model.global.basic.schedule rt.model.global.basic.interference
+               rt.model.global.basic.platform.
+Require Import rt.analysis.global.parallel.workload_bound
+               rt.analysis.global.parallel.interference_bound_edf.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
 
 Module ResponseTimeAnalysisEDF.
diff --git a/analysis/parallel/bertogna_fp_comp.v b/analysis/global/parallel/bertogna_fp_comp.v
similarity index 99%
rename from analysis/parallel/bertogna_fp_comp.v
rename to analysis/global/parallel/bertogna_fp_comp.v
index 0656ea907532feef14f5728cf3742e3670f9dfec..b7fa67b9bd06082621918d7bd2e4748f84d699ca 100644
--- a/analysis/parallel/bertogna_fp_comp.v
+++ b/analysis/global/parallel/bertogna_fp_comp.v
@@ -1,5 +1,5 @@
 Require Import rt.util.all.
-Require Import rt.analysis.parallel.bertogna_fp_theory.
+Require Import rt.analysis.global.parallel.bertogna_fp_theory.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop div path.
 
 Module ResponseTimeIterationFP.
diff --git a/analysis/parallel/bertogna_fp_theory.v b/analysis/global/parallel/bertogna_fp_theory.v
similarity index 97%
rename from analysis/parallel/bertogna_fp_theory.v
rename to analysis/global/parallel/bertogna_fp_theory.v
index 64db0dab1d0555c677e850f6d24fce68472312ea..71941b6c2519e43af4d0777ab7f4f88ca32be8ed 100644
--- a/analysis/parallel/bertogna_fp_theory.v
+++ b/analysis/global/parallel/bertogna_fp_theory.v
@@ -1,11 +1,11 @@
 Require Import rt.util.all.
-Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.task_arrival
-               rt.model.basic.schedule rt.model.basic.platform
-               rt.model.basic.constrained_deadlines
-               rt.model.basic.workload rt.model.basic.schedulability
-               rt.model.basic.priority rt.model.basic.response_time
-               rt.model.basic.interference.
-Require Import rt.analysis.parallel.workload_bound rt.analysis.parallel.interference_bound_fp.
+Require Import rt.model.task rt.model.job rt.model.task_arrival
+        rt.model.priority.
+Require Import rt.model.global.workload rt.model.global.schedulability
+               rt.model.global.response_time.
+Require Import rt.model.global.basic.schedule rt.model.global.basic.platform
+               rt.model.global.basic.constrained_deadlines rt.model.global.basic.interference.
+Require Import rt.analysis.global.parallel.workload_bound rt.analysis.global.parallel.interference_bound_fp.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
 
 Module ResponseTimeAnalysisFP.
diff --git a/analysis/parallel/interference_bound.v b/analysis/global/parallel/interference_bound.v
similarity index 91%
rename from analysis/parallel/interference_bound.v
rename to analysis/global/parallel/interference_bound.v
index 63fed92913d98b4ac6e3698adff0d1c61510feeb..28a7e8a632d5e4da61443075858a9d8298e1cd01 100644
--- a/analysis/parallel/interference_bound.v
+++ b/analysis/global/parallel/interference_bound.v
@@ -1,6 +1,6 @@
 Require Import rt.util.all.
-Require Import rt.model.basic.schedule.
-Require Import rt.analysis.parallel.workload_bound.
+Require Import rt.model.global.basic.schedule.
+Require Import rt.analysis.global.parallel.workload_bound.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 Module InterferenceBoundGeneric.
diff --git a/analysis/parallel/interference_bound_edf.v b/analysis/global/parallel/interference_bound_edf.v
similarity index 98%
rename from analysis/parallel/interference_bound_edf.v
rename to analysis/global/parallel/interference_bound_edf.v
index f0f2c6a33ef959c913e9e2efde66b0d6385869f1..4b11160f4a12c9f04d7a2ab0b9a8733bf0e16313 100644
--- a/analysis/parallel/interference_bound_edf.v
+++ b/analysis/global/parallel/interference_bound_edf.v
@@ -1,9 +1,11 @@
 Require Import rt.util.all.
-Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.schedule
-               rt.model.basic.task_arrival rt.model.basic.platform rt.model.basic.response_time
-               rt.model.basic.workload rt.model.basic.priority rt.model.basic.schedulability
-               rt.model.basic.interference rt.model.basic.interference_edf.
-Require Import rt.analysis.parallel.workload_bound rt.analysis.parallel.interference_bound.
+Require Import rt.model.task rt.model.job rt.model.priority rt.model.task_arrival.
+Require Import rt.model.global.response_time rt.model.global.workload
+               rt.model.global.schedulability.
+Require Import rt.model.global.basic.schedule rt.model.global.basic.platform
+               rt.model.global.basic.interference rt.model.global.basic.interference_edf.
+Require Import rt.analysis.global.parallel.workload_bound
+               rt.analysis.global.parallel.interference_bound.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
 
 Module InterferenceBoundEDF.
diff --git a/analysis/parallel/interference_bound_fp.v b/analysis/global/parallel/interference_bound_fp.v
similarity index 83%
rename from analysis/parallel/interference_bound_fp.v
rename to analysis/global/parallel/interference_bound_fp.v
index e6aa91d6f47fb2a8697b2f49c1ef12103d4509ac..e976b390e7378319f042c7dea5cc3d74615e6a21 100644
--- a/analysis/parallel/interference_bound_fp.v
+++ b/analysis/global/parallel/interference_bound_fp.v
@@ -1,7 +1,8 @@
 Require Import rt.util.all.
-Require Import rt.model.basic.schedule rt.model.basic.priority rt.model.basic.workload
-               rt.model.basic.interference.
-Require Import rt.analysis.parallel.workload_bound rt.analysis.parallel.interference_bound.
+Require Import rt.model.priority.
+Require Import rt.model.global.workload.
+Require Import rt.model.global.basic.schedule rt.model.global.basic.interference.
+Require Import rt.analysis.global.parallel.workload_bound rt.analysis.global.parallel.interference_bound.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 Module InterferenceBoundFP.
diff --git a/analysis/parallel/workload_bound.v b/analysis/global/parallel/workload_bound.v
similarity index 98%
rename from analysis/parallel/workload_bound.v
rename to analysis/global/parallel/workload_bound.v
index 6cae44aec99594d0e10902b2cf81a1892b311f03..ea291fb193c62ed1c3a285b3d3c6874caefe2ba1 100644
--- a/analysis/parallel/workload_bound.v
+++ b/analysis/global/parallel/workload_bound.v
@@ -1,7 +1,8 @@
 Require Import rt.util.all.
-Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.schedule
-               rt.model.basic.task_arrival rt.model.basic.response_time
-               rt.model.basic.workload rt.model.basic.schedulability.
+Require Import rt.model.task rt.model.job rt.model.task_arrival.
+Require Import rt.model.global.response_time rt.model.global.workload
+               rt.model.global.schedulability.
+Require Import rt.model.global.basic.schedule.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq div fintype bigop path.
 
 Module WorkloadBound.
diff --git a/implementation/apa/arrival_sequence.v b/implementation/apa/arrival_sequence.v
index ef341ef736b8aead9ec9edd34fd04c931bea6d0d..ddee41bb35418bee1bdfe31bd6512f6f439ea119 100644
--- a/implementation/apa/arrival_sequence.v
+++ b/implementation/apa/arrival_sequence.v
@@ -1,7 +1,6 @@
 (* We can reuse the.apa definition of periodic arrival sequence. *)
 Require Import rt.util.all.
-Require Import rt.model.apa.arrival_sequence rt.model.apa.job
-               rt.model.apa.task rt.model.apa.task_arrival.
+Require Import rt.model.arrival_sequence rt.model.job rt.model.task rt.model.task_arrival.
 Require Import rt.implementation.apa.task rt.implementation.apa.job.
 From mathcomp Require Import ssreflect ssrbool ssrfun ssrnat eqtype seq div.
 
diff --git a/implementation/apa/bertogna_edf_example.v b/implementation/apa/bertogna_edf_example.v
index c922446a9cdcf616e4f20d8c09f9ded1b772f84c..98defcb390cef535c77ab30a6c7aeaf1a75c2b49 100644
--- a/implementation/apa/bertogna_edf_example.v
+++ b/implementation/apa/bertogna_edf_example.v
@@ -1,8 +1,8 @@
 Require Import rt.util.all.
-Require Import rt.model.apa.job rt.model.apa.task rt.model.apa.affinity
-               rt.model.apa.schedule rt.model.apa.interference
-               rt.model.apa.schedulability
-               rt.model.apa.priority rt.model.apa.platform.
+Require Import rt.model.job rt.model.task rt.model.priority.
+Require Import rt.model.global.schedulability.
+Require Import rt.model.global.basic.schedule.
+Require Import rt.model.apa.affinity rt.model.apa.interference rt.model.apa.platform.
 Require Import rt.analysis.apa.workload_bound
                rt.analysis.apa.interference_bound_edf
                rt.analysis.apa.bertogna_edf_comp.
diff --git a/implementation/apa/bertogna_fp_example.v b/implementation/apa/bertogna_fp_example.v
index e2dc3f5470dfad42812aaf37f81163cf36be2601..4896677a6a63afc5cd35ab0d4d3dce1c79250f5a 100644
--- a/implementation/apa/bertogna_fp_example.v
+++ b/implementation/apa/bertogna_fp_example.v
@@ -1,8 +1,8 @@
 Require Import rt.util.all.
-Require Import rt.model.apa.job rt.model.apa.task rt.model.apa.affinity
-               rt.model.apa.schedule rt.model.apa.schedulability
-               rt.model.apa.priority rt.model.apa.platform
-               rt.model.apa.interference.
+Require Import rt.model.job rt.model.task rt.model.priority.
+Require Import rt.model.global.schedulability.
+Require Import rt.model.global.basic.schedule.
+Require Import rt.model.apa.affinity rt.model.apa.interference rt.model.apa.platform.
 Require Import rt.analysis.apa.workload_bound
                rt.analysis.apa.interference_bound_fp
                rt.analysis.apa.bertogna_fp_comp.
diff --git a/implementation/apa/job.v b/implementation/apa/job.v
index bf22a52aca85ee2489c0b591eb14e871252defd6..1bb33947092ccaee4ca563aac82b8547d8e57623 100644
--- a/implementation/apa/job.v
+++ b/implementation/apa/job.v
@@ -1,4 +1,4 @@
-Require Import rt.model.basic.time rt.util.all.
+Require Import rt.model.time rt.util.all.
 Require Import rt.implementation.apa.task.
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq.
 
diff --git a/implementation/apa/schedule.v b/implementation/apa/schedule.v
index 80014bdb26b6f64c3c677a86fcd5256ca7fab092..266e6d6e7e437a23f292cd52751981426b7f126a 100644
--- a/implementation/apa/schedule.v
+++ b/implementation/apa/schedule.v
@@ -1,7 +1,8 @@
 Require Import rt.util.all.
-Require Import rt.model.apa.job rt.model.apa.task rt.model.apa.affinity
-               rt.model.apa.arrival_sequence rt.model.apa.schedule
-               rt.model.apa.platform rt.model.apa.priority.
+Require Import rt.model.arrival_sequence rt.model.job rt.model.task rt.model.priority
+               rt.model.task_arrival.
+Require Import rt.model.global.basic.schedule.
+Require Import rt.model.apa.affinity rt.model.apa.platform.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat fintype bigop seq path.
 
 Module ConcreteScheduler.
diff --git a/implementation/apa/task.v b/implementation/apa/task.v
index 6281667a82afba5ce8fc63344a14a821cdf349eb..e5f35650181e3425b8faa7e0af6f2d758084bc32 100644
--- a/implementation/apa/task.v
+++ b/implementation/apa/task.v
@@ -1,5 +1,6 @@
-Require Import rt.model.apa.time rt.util.all.
-Require Import rt.model.apa.task rt.model.apa.affinity.
+Require Import rt.util.all.
+Require Import rt.model.time rt.model.task.
+Require Import rt.model.apa.affinity.
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq.
 
 Module ConcreteTask.
diff --git a/implementation/basic/arrival_sequence.v b/implementation/global/basic/arrival_sequence.v
similarity index 95%
rename from implementation/basic/arrival_sequence.v
rename to implementation/global/basic/arrival_sequence.v
index 8e17a0d7c800293f0007b668ee29097ccb145912..22f97bb7fa68eef60515c6d261fa40684cb5ed25 100644
--- a/implementation/basic/arrival_sequence.v
+++ b/implementation/global/basic/arrival_sequence.v
@@ -1,7 +1,7 @@
 Require Import rt.util.all.
-Require Import rt.model.basic.arrival_sequence rt.model.basic.job
-               rt.model.basic.task rt.model.basic.task_arrival.
-Require Import rt.implementation.basic.task rt.implementation.basic.job.
+Require Import rt.model.arrival_sequence rt.model.job
+               rt.model.task rt.model.task_arrival.
+Require Import rt.implementation.global.basic.task rt.implementation.global.basic.job.
 From mathcomp Require Import ssreflect ssrbool ssrfun ssrnat eqtype seq div.
 
 Module ConcreteArrivalSequence.
diff --git a/implementation/basic/bertogna_edf_example.v b/implementation/global/basic/bertogna_edf_example.v
similarity index 89%
rename from implementation/basic/bertogna_edf_example.v
rename to implementation/global/basic/bertogna_edf_example.v
index dfd5e8f997dc692e3435e86cf05d931fa21caa32..b418fd885b8019f43c777cbaa5e392d6fc7959ee 100644
--- a/implementation/basic/bertogna_edf_example.v
+++ b/implementation/global/basic/bertogna_edf_example.v
@@ -1,14 +1,14 @@
 Require Import rt.util.all.
-Require Import rt.model.basic.job rt.model.basic.task
-               rt.model.basic.schedule rt.model.basic.schedulability
-               rt.model.basic.priority rt.model.basic.platform.
-Require Import rt.analysis.basic.workload_bound
-               rt.analysis.basic.interference_bound_edf
-               rt.analysis.basic.bertogna_edf_comp.
-Require Import rt.implementation.basic.job
-               rt.implementation.basic.task
-               rt.implementation.basic.schedule
-               rt.implementation.basic.arrival_sequence.
+Require Import rt.model.job rt.model.task rt.model.priority.
+Require Import rt.model.global.schedulability.
+Require Import rt.model.global.basic.schedule rt.model.global.basic.platform.
+Require Import rt.analysis.global.basic.workload_bound
+               rt.analysis.global.basic.interference_bound_edf
+               rt.analysis.global.basic.bertogna_edf_comp.
+Require Import rt.implementation.global.basic.job
+               rt.implementation.global.basic.task
+               rt.implementation.global.basic.schedule
+               rt.implementation.global.basic.arrival_sequence.
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq bigop div.
 
 Module ResponseTimeAnalysisEDF.
diff --git a/implementation/basic/bertogna_fp_example.v b/implementation/global/basic/bertogna_fp_example.v
similarity index 91%
rename from implementation/basic/bertogna_fp_example.v
rename to implementation/global/basic/bertogna_fp_example.v
index e6f766bb79d318a4869a61bf3a2e0d6f073ff1d3..173131feafc4ae586967c82f5fe22225221c07e4 100644
--- a/implementation/basic/bertogna_fp_example.v
+++ b/implementation/global/basic/bertogna_fp_example.v
@@ -1,14 +1,14 @@
 Require Import rt.util.all.
-Require Import rt.model.basic.job rt.model.basic.task
-               rt.model.basic.schedule rt.model.basic.schedulability
-               rt.model.basic.priority rt.model.basic.platform.
-Require Import rt.analysis.basic.workload_bound
-               rt.analysis.basic.interference_bound_fp
-               rt.analysis.basic.bertogna_fp_comp.
-Require Import rt.implementation.basic.job
-               rt.implementation.basic.task
-               rt.implementation.basic.schedule
-               rt.implementation.basic.arrival_sequence.
+Require Import rt.model.job rt.model.task rt.model.priority.
+Require Import rt.model.global.schedulability.
+Require Import rt.model.global.basic.schedule rt.model.global.basic.platform.
+Require Import rt.analysis.global.basic.workload_bound
+               rt.analysis.global.basic.interference_bound_fp
+               rt.analysis.global.basic.bertogna_fp_comp.
+Require Import rt.implementation.global.basic.job
+               rt.implementation.global.basic.task
+               rt.implementation.global.basic.schedule
+               rt.implementation.global.basic.arrival_sequence.
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq bigop div.
 
 Module ResponseTimeAnalysisFP.
diff --git a/implementation/basic/job.v b/implementation/global/basic/job.v
similarity index 95%
rename from implementation/basic/job.v
rename to implementation/global/basic/job.v
index db1a3c372939e72e20b185dc6382b143d96f3e4e..cd24f6d855bf6b91bab27e8b8d054cb1d716eb53 100644
--- a/implementation/basic/job.v
+++ b/implementation/global/basic/job.v
@@ -1,5 +1,5 @@
-Require Import rt.model.basic.time rt.util.all.
-Require Import rt.implementation.basic.task.
+Require Import rt.model.time rt.util.all.
+Require Import rt.implementation.global.basic.task.
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq.
 
 Module ConcreteJob.
diff --git a/implementation/basic/schedule.v b/implementation/global/basic/schedule.v
similarity index 98%
rename from implementation/basic/schedule.v
rename to implementation/global/basic/schedule.v
index 99adb9705ae30763e257aa572e2edc0812d9fd09..a8df880d0976838bc23e071dbd66069810c56068 100644
--- a/implementation/basic/schedule.v
+++ b/implementation/global/basic/schedule.v
@@ -1,6 +1,6 @@
 Require Import rt.util.all.
-Require Import rt.model.basic.job rt.model.basic.arrival_sequence rt.model.basic.schedule
-               rt.model.basic.platform rt.model.basic.priority.
+Require Import rt.model.job rt.model.arrival_sequence rt.model.priority.
+Require Import rt.model.global.basic.schedule rt.model.global.basic.platform.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat fintype bigop seq path.
 
 Module ConcreteScheduler.
diff --git a/implementation/basic/task.v b/implementation/global/basic/task.v
similarity index 95%
rename from implementation/basic/task.v
rename to implementation/global/basic/task.v
index fe158837bc9def7383f85be212782bbc596ea5f9..532e4bcbf9e6efe973aec4758b22397160c53688 100644
--- a/implementation/basic/task.v
+++ b/implementation/global/basic/task.v
@@ -1,5 +1,5 @@
-Require Import rt.model.basic.time rt.util.all.
-Require Import rt.model.basic.task.
+Require Import rt.model.time rt.util.all.
+Require Import rt.model.task.
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq.
 
 Module ConcreteTask.
diff --git a/implementation/jitter/arrival_sequence.v b/implementation/global/jitter/arrival_sequence.v
similarity index 95%
rename from implementation/jitter/arrival_sequence.v
rename to implementation/global/jitter/arrival_sequence.v
index 4fb3a3c96291b0a2082cce8a934d8b7c5a060a8a..90d5b8b9b8f30d96d7aa5789e9c944287739a202 100644
--- a/implementation/jitter/arrival_sequence.v
+++ b/implementation/global/jitter/arrival_sequence.v
@@ -1,7 +1,7 @@
 Require Import rt.util.all.
-Require Import rt.model.jitter.arrival_sequence rt.model.jitter.job
-               rt.model.jitter.task rt.model.jitter.task_arrival.
-Require Import rt.implementation.jitter.task rt.implementation.jitter.job.
+Require Import rt.model.arrival_sequence rt.model.task rt.model.task_arrival.
+Require Import rt.model.global.jitter.job.
+Require Import rt.implementation.global.jitter.task rt.implementation.global.jitter.job.
 From mathcomp Require Import ssreflect ssrbool ssrfun ssrnat eqtype seq div.
 
 Module ConcreteArrivalSequence.
diff --git a/implementation/jitter/bertogna_edf_example.v b/implementation/global/jitter/bertogna_edf_example.v
similarity index 88%
rename from implementation/jitter/bertogna_edf_example.v
rename to implementation/global/jitter/bertogna_edf_example.v
index 4763d22d9d62250964e0b04dfd872600b2decdb8..384b64c0b8e9e1ae84042641f0d83f5de8bf4bd9 100644
--- a/implementation/jitter/bertogna_edf_example.v
+++ b/implementation/global/jitter/bertogna_edf_example.v
@@ -1,14 +1,15 @@
 Require Import rt.util.all.
-Require Import rt.model.jitter.job rt.model.jitter.task
-               rt.model.jitter.schedule rt.model.jitter.schedulability
-               rt.model.jitter.priority rt.model.jitter.platform.
-Require Import rt.analysis.jitter.workload_bound
-               rt.analysis.jitter.interference_bound_edf
-               rt.analysis.jitter.bertogna_edf_comp.
-Require Import rt.implementation.jitter.job
-               rt.implementation.jitter.task
-               rt.implementation.jitter.schedule
-               rt.implementation.jitter.arrival_sequence.
+Require Import rt.model.task rt.model.priority.
+Require Import rt.model.global.schedulability.
+Require Import rt.model.global.jitter.job rt.model.global.jitter.schedule
+               rt.model.global.jitter.platform.
+Require Import rt.analysis.global.jitter.workload_bound
+               rt.analysis.global.jitter.interference_bound_edf
+               rt.analysis.global.jitter.bertogna_edf_comp.
+Require Import rt.implementation.global.jitter.job
+               rt.implementation.global.jitter.task
+               rt.implementation.global.jitter.schedule
+               rt.implementation.global.jitter.arrival_sequence.
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq bigop div.
 
 Module ResponseTimeAnalysisEDF.
diff --git a/implementation/jitter/bertogna_fp_example.v b/implementation/global/jitter/bertogna_fp_example.v
similarity index 91%
rename from implementation/jitter/bertogna_fp_example.v
rename to implementation/global/jitter/bertogna_fp_example.v
index da15c4d31850879ac7f42a42dd3f6f275443b807..023dc7bd9f7ffd82a2f0c9003a55192f68614b73 100644
--- a/implementation/jitter/bertogna_fp_example.v
+++ b/implementation/global/jitter/bertogna_fp_example.v
@@ -1,14 +1,15 @@
 Require Import rt.util.all.
-Require Import rt.model.jitter.job rt.model.jitter.task
-               rt.model.jitter.schedule rt.model.jitter.schedulability
-               rt.model.jitter.priority rt.model.jitter.platform.
-Require Import rt.analysis.jitter.workload_bound
-               rt.analysis.jitter.interference_bound_fp
-               rt.analysis.jitter.bertogna_fp_comp.
-Require Import rt.implementation.jitter.job
-               rt.implementation.jitter.task
-               rt.implementation.jitter.schedule
-               rt.implementation.jitter.arrival_sequence.
+Require Import rt.model.task rt.model.priority.
+Require Import rt.model.global.schedulability.
+Require Import rt.model.global.jitter.job rt.model.global.jitter.schedule
+               rt.model.global.jitter.platform.
+Require Import rt.analysis.global.jitter.workload_bound
+               rt.analysis.global.jitter.interference_bound_fp
+               rt.analysis.global.jitter.bertogna_fp_comp.
+Require Import rt.implementation.global.jitter.job
+               rt.implementation.global.jitter.task
+               rt.implementation.global.jitter.schedule
+               rt.implementation.global.jitter.arrival_sequence.
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq bigop div.
 
 Module ResponseTimeAnalysisFP.
diff --git a/implementation/jitter/job.v b/implementation/global/jitter/job.v
similarity index 97%
rename from implementation/jitter/job.v
rename to implementation/global/jitter/job.v
index 3eb0633ca68f781c5cd1404fedaa830410dd1783..abe5e300ac5f2434ed0d3925a1e75a25e7741317 100644
--- a/implementation/jitter/job.v
+++ b/implementation/global/jitter/job.v
@@ -1,5 +1,5 @@
 Require Import rt.util.all.
-Require Import rt.implementation.jitter.task.
+Require Import rt.implementation.global.jitter.task.
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq.
 
 Module ConcreteJob.
diff --git a/implementation/jitter/schedule.v b/implementation/global/jitter/schedule.v
similarity index 98%
rename from implementation/jitter/schedule.v
rename to implementation/global/jitter/schedule.v
index 58268053bcb3214be63db02c1fed4f24b1f7f721..ebee74bee7a79fbe31b2e2a0edf72f8f9b62921e 100644
--- a/implementation/jitter/schedule.v
+++ b/implementation/global/jitter/schedule.v
@@ -1,6 +1,7 @@
 Require Import rt.util.all.
-Require Import rt.model.jitter.job rt.model.jitter.arrival_sequence rt.model.jitter.schedule
-               rt.model.jitter.platform rt.model.jitter.priority.
+Require Import rt.model.arrival_sequence rt.model.priority.
+Require Import rt.model.global.jitter.job rt.model.global.jitter.schedule
+               rt.model.global.jitter.platform.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat fintype bigop seq path.
 
 Module ConcreteScheduler.
diff --git a/implementation/jitter/task.v b/implementation/global/jitter/task.v
similarity index 98%
rename from implementation/jitter/task.v
rename to implementation/global/jitter/task.v
index 4e0238f398222124292718ef810c58c88b52cc74..07802b708a2f78065ae48098a980dc261b46ad77 100644
--- a/implementation/jitter/task.v
+++ b/implementation/global/jitter/task.v
@@ -1,5 +1,5 @@
 Require Import rt.util.all.
-Require Import rt.model.jitter.task.
+Require Import rt.model.task.
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq.
 
 Module ConcreteTask.
diff --git a/implementation/global/parallel/arrival_sequence.v b/implementation/global/parallel/arrival_sequence.v
new file mode 100644
index 0000000000000000000000000000000000000000..8d51d82cb24e9b1370428fc5ce8a3b18abeb95f5
--- /dev/null
+++ b/implementation/global/parallel/arrival_sequence.v
@@ -0,0 +1,2 @@
+(* We reuse the arrival sequence from the basic model. *)
+Require Export rt.implementation.global.basic.arrival_sequence.
\ No newline at end of file
diff --git a/implementation/parallel/bertogna_edf_example.v b/implementation/global/parallel/bertogna_edf_example.v
similarity index 89%
rename from implementation/parallel/bertogna_edf_example.v
rename to implementation/global/parallel/bertogna_edf_example.v
index d2398d72dfb56eee18c09e904ca63322e1567b50..cb7793c137b5095cf150d10dd982a89b1c5d3a6a 100644
--- a/implementation/parallel/bertogna_edf_example.v
+++ b/implementation/global/parallel/bertogna_edf_example.v
@@ -1,14 +1,14 @@
 Require Import rt.util.all.
-Require Import rt.model.basic.job rt.model.basic.task
-               rt.model.basic.schedule rt.model.basic.schedulability
-               rt.model.basic.priority rt.model.basic.platform.
-Require Import rt.analysis.parallel.workload_bound
-               rt.analysis.parallel.interference_bound_edf
-               rt.analysis.parallel.bertogna_edf_comp.
-Require Import rt.implementation.parallel.job
-               rt.implementation.parallel.task
-               rt.implementation.parallel.schedule
-               rt.implementation.parallel.arrival_sequence.
+Require Import rt.model.job rt.model.task rt.model.priority.
+Require Import rt.model.global.schedulability.
+Require Import rt.model.global.basic.schedule rt.model.global.basic.platform.
+Require Import rt.analysis.global.parallel.workload_bound
+               rt.analysis.global.parallel.interference_bound_edf
+               rt.analysis.global.parallel.bertogna_edf_comp.
+Require Import rt.implementation.global.parallel.job
+               rt.implementation.global.parallel.task
+               rt.implementation.global.parallel.schedule
+               rt.implementation.global.parallel.arrival_sequence.
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq bigop div.
 
 Module ResponseTimeAnalysisEDF.
diff --git a/implementation/parallel/bertogna_fp_example.v b/implementation/global/parallel/bertogna_fp_example.v
similarity index 91%
rename from implementation/parallel/bertogna_fp_example.v
rename to implementation/global/parallel/bertogna_fp_example.v
index aef7d69a421cfa65b501ffb7ef62d2de9e15e17a..630eb6c02b9b38145084a5e5e1d60afe6b3e6a49 100644
--- a/implementation/parallel/bertogna_fp_example.v
+++ b/implementation/global/parallel/bertogna_fp_example.v
@@ -1,15 +1,15 @@
 Require Import rt.util.all.
-Require Import rt.model.basic.job rt.model.basic.task
-               rt.model.basic.schedule rt.model.basic.schedulability
-               rt.model.basic.priority rt.model.basic.platform
-               rt.model.basic.interference.
-Require Import rt.analysis.parallel.workload_bound
-               rt.analysis.parallel.interference_bound_fp
-               rt.analysis.parallel.bertogna_fp_comp.
-Require Import rt.implementation.parallel.job
-               rt.implementation.parallel.task
-               rt.implementation.parallel.schedule
-               rt.implementation.parallel.arrival_sequence.
+Require Import rt.model.job rt.model.task rt.model.priority.
+Require Import rt.model.global.schedulability.
+Require Import rt.model.global.basic.schedule rt.model.global.basic.platform
+               rt.model.global.basic.interference.
+Require Import rt.analysis.global.parallel.workload_bound
+               rt.analysis.global.parallel.interference_bound_fp
+               rt.analysis.global.parallel.bertogna_fp_comp.
+Require Import rt.implementation.global.parallel.job
+               rt.implementation.global.parallel.task
+               rt.implementation.global.parallel.schedule
+               rt.implementation.global.parallel.arrival_sequence.
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq bigop div.
 
 Module ResponseTimeAnalysisFP.
diff --git a/implementation/global/parallel/job.v b/implementation/global/parallel/job.v
new file mode 100644
index 0000000000000000000000000000000000000000..db7513c161a30592686060968db4a62345196fbe
--- /dev/null
+++ b/implementation/global/parallel/job.v
@@ -0,0 +1,2 @@
+(* We reuse the job from the basic model. *)
+Require Export rt.implementation.global.basic.job.
\ No newline at end of file
diff --git a/implementation/parallel/schedule.v b/implementation/global/parallel/schedule.v
similarity index 74%
rename from implementation/parallel/schedule.v
rename to implementation/global/parallel/schedule.v
index fdfac70394bc838fd58d19c473fd11d69a513052..81cf6706736c3c5244161f3df872f3840c0c226d 100644
--- a/implementation/parallel/schedule.v
+++ b/implementation/global/parallel/schedule.v
@@ -1,4 +1,4 @@
 (* For simplicity, we reuse the scheduler from the basic model.
    Although it does not exploit parallelism, it is a restricted case
    of a parallel scheduler. *)
-Require Export rt.implementation.basic.schedule.
\ No newline at end of file
+Require Export rt.implementation.global.basic.schedule.
\ No newline at end of file
diff --git a/implementation/global/parallel/task.v b/implementation/global/parallel/task.v
new file mode 100644
index 0000000000000000000000000000000000000000..d176fe900a1e32b39ac79280d460e9b63ad02ed6
--- /dev/null
+++ b/implementation/global/parallel/task.v
@@ -0,0 +1,2 @@
+(* We reuse the task from the basic model. *)
+Require Export rt.implementation.global.basic.task.
\ No newline at end of file
diff --git a/implementation/parallel/arrival_sequence.v b/implementation/parallel/arrival_sequence.v
deleted file mode 100644
index 4f6f2213a1a2cd21ca461cb2a122425adea7f1a3..0000000000000000000000000000000000000000
--- a/implementation/parallel/arrival_sequence.v
+++ /dev/null
@@ -1,2 +0,0 @@
-(* We reuse the arrival sequence from the basic model. *)
-Require Export rt.implementation.basic.arrival_sequence.
\ No newline at end of file
diff --git a/implementation/parallel/job.v b/implementation/parallel/job.v
deleted file mode 100644
index 78b0bd655db83854403535830cdf828d6329ce74..0000000000000000000000000000000000000000
--- a/implementation/parallel/job.v
+++ /dev/null
@@ -1,2 +0,0 @@
-(* We reuse the job from the basic model. *)
-Require Export rt.implementation.basic.job.
\ No newline at end of file
diff --git a/implementation/parallel/task.v b/implementation/parallel/task.v
deleted file mode 100644
index d4eb8e27de636a10883885260ff913d298a0d176..0000000000000000000000000000000000000000
--- a/implementation/parallel/task.v
+++ /dev/null
@@ -1,2 +0,0 @@
-(* We reuse the task from the basic model. *)
-Require Export rt.implementation.basic.task.
\ No newline at end of file
diff --git a/model/apa/affinity.v b/model/apa/affinity.v
index f819d86a54368335431d9f00c1c9df3e96a52568..3d670dbc8b937a03ed5b18ebe539825614d05153 100644
--- a/model/apa/affinity.v
+++ b/model/apa/affinity.v
@@ -1,6 +1,6 @@
 Require Import rt.util.all.
-Require Import rt.model.apa.job rt.model.apa.task
-               rt.model.apa.arrival_sequence rt.model.apa.schedule.
+Require Import rt.model.job rt.model.task rt.model.arrival_sequence.
+Require Import rt.model.global.basic.schedule.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 (* Definition and properties about processor affinities. *)
diff --git a/model/apa/arrival_sequence.v b/model/apa/arrival_sequence.v
deleted file mode 100644
index 0ab7d9296238e824a51fce508cb97454946058c9..0000000000000000000000000000000000000000
--- a/model/apa/arrival_sequence.v
+++ /dev/null
@@ -1,2 +0,0 @@
-(* The arrival sequence remains the same under APA scheduling. *)
-Require Export rt.model.basic.arrival_sequence.
\ No newline at end of file
diff --git a/model/apa/constrained_deadlines.v b/model/apa/constrained_deadlines.v
index 55b1abc631378c74b5becd5dc033e357a2d6d69d..d4811fd12f5f6e84cad14b23618ae26fccc0c6f9 100644
--- a/model/apa/constrained_deadlines.v
+++ b/model/apa/constrained_deadlines.v
@@ -1,8 +1,7 @@
 Require Import rt.util.all.
-Require Import rt.model.apa.task rt.model.apa.job rt.model.apa.schedule
-               rt.model.apa.priority rt.model.apa.task_arrival
-               rt.model.apa.interference rt.model.apa.affinity
-               rt.model.apa.platform.
+Require Import rt.model.job rt.model.task rt.model.priority rt.model.task_arrival.
+Require Import rt.model.global.basic.schedule.
+Require Import rt.model.apa.interference rt.model.apa.affinity rt.model.apa.platform.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
 Module ConstrainedDeadlines.
diff --git a/model/apa/interference.v b/model/apa/interference.v
index f0a2fe842157a8bb5b8006fa23e7e8fe2a7bac30..f566b65534411d02683989e1d641a8dbdcbd0ff1 100644
--- a/model/apa/interference.v
+++ b/model/apa/interference.v
@@ -1,6 +1,8 @@
 Require Import rt.util.all rt.util.divround.
-Require Import rt.model.apa.task rt.model.apa.job rt.model.apa.schedule
-               rt.model.apa.priority rt.model.apa.workload rt.model.apa.affinity.
+Require Import rt.model.job rt.model.task rt.model.priority.
+Require Import rt.model.global.workload.
+Require Import rt.model.global.basic.schedule.
+Require Import rt.model.apa.affinity.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 Module Interference.
diff --git a/model/apa/interference_edf.v b/model/apa/interference_edf.v
index c1bb429ec65ae6116bf906f6750c1e82940665c4..fcd1ee9df640e7555ab679ff2f366e3ac1ed8612 100644
--- a/model/apa/interference_edf.v
+++ b/model/apa/interference_edf.v
@@ -1,8 +1,8 @@
 Require Import rt.util.all.
-Require Import rt.model.apa.task rt.model.apa.job rt.model.apa.schedule
-               rt.model.apa.priority rt.model.apa.task_arrival rt.model.apa.interference
-               rt.model.apa.arrival_sequence rt.model.apa.platform
-               rt.model.apa.affinity.
+Require Import rt.model.task rt.model.job rt.model.priority rt.model.task_arrival.
+Require Import rt.model.global.basic.schedule.
+Require Import rt.model.apa.affinity rt.model.apa.interference
+               rt.model.apa.platform.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
 Module InterferenceEDF.
diff --git a/model/apa/job.v b/model/apa/job.v
deleted file mode 100644
index 3e6878902b7da1994119dd724869a2e3baa0d599..0000000000000000000000000000000000000000
--- a/model/apa/job.v
+++ /dev/null
@@ -1,2 +0,0 @@
-(* The notion of a valid job remains the same under APA scheduling. *)
-Require Export rt.model.basic.job.
\ No newline at end of file
diff --git a/model/apa/platform.v b/model/apa/platform.v
index d734339292813ac5390e93d4770c3e184a6dedd0..3399e330eadd2c21c2f37b9c1e57ad3480b4b28d 100644
--- a/model/apa/platform.v
+++ b/model/apa/platform.v
@@ -1,7 +1,7 @@
 Require Import rt.util.all.
-Require Import rt.model.apa.task rt.model.apa.job rt.model.apa.schedule
-               rt.model.apa.priority rt.model.apa.task_arrival
-               rt.model.apa.interference rt.model.apa.affinity.
+Require Import rt.model.job rt.model.task rt.model.priority rt.model.task_arrival.
+Require Import rt.model.global.basic.schedule.
+Require Import rt.model.apa.interference rt.model.apa.affinity.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
 Module Platform.
diff --git a/model/apa/priority.v b/model/apa/priority.v
deleted file mode 100644
index ee2fe4187ad5f9e099450d57026e0a05ede7c0cf..0000000000000000000000000000000000000000
--- a/model/apa/priority.v
+++ /dev/null
@@ -1,2 +0,0 @@
-(* The definition of priority remains the same under APA scheduling. *)
-Require Export rt.model.basic.priority.
\ No newline at end of file
diff --git a/model/apa/response_time.v b/model/apa/response_time.v
deleted file mode 100644
index 06c3c32c6294099338ab2e33f00382a08a44487c..0000000000000000000000000000000000000000
--- a/model/apa/response_time.v
+++ /dev/null
@@ -1,2 +0,0 @@
-(* The definition of response time remains the same under APA scheduling. *)
-Require Export rt.model.basic.response_time.
\ No newline at end of file
diff --git a/model/apa/schedulability.v b/model/apa/schedulability.v
deleted file mode 100644
index db9b150a58cc5222236c5269952218bb7abe79c4..0000000000000000000000000000000000000000
--- a/model/apa/schedulability.v
+++ /dev/null
@@ -1,2 +0,0 @@
-(* The notion of schedulability remains the same under APA scheduling. *)
-Require Export rt.model.basic.schedulability.
\ No newline at end of file
diff --git a/model/apa/schedule.v b/model/apa/schedule.v
deleted file mode 100644
index 80aa78b0d6d4d096740ddce3a839fdf3b14a7d2e..0000000000000000000000000000000000000000
--- a/model/apa/schedule.v
+++ /dev/null
@@ -1,2 +0,0 @@
-(* The definition of schedule remains the same under APA scheduling. *)
-Require Export rt.model.basic.schedule.
\ No newline at end of file
diff --git a/model/apa/task.v b/model/apa/task.v
deleted file mode 100644
index 12257fa0840d540106f3908d33a0190d24ec37fa..0000000000000000000000000000000000000000
--- a/model/apa/task.v
+++ /dev/null
@@ -1,2 +0,0 @@
-(* The notion of a valid task remains the same under APA scheduling. *)
-Require Export rt.model.basic.task.
\ No newline at end of file
diff --git a/model/apa/task_arrival.v b/model/apa/task_arrival.v
deleted file mode 100644
index d7299e0141593fe1e59ad6a3ebc964267bde4af5..0000000000000000000000000000000000000000
--- a/model/apa/task_arrival.v
+++ /dev/null
@@ -1,2 +0,0 @@
-(* The notion of interarrival times does not change under APA scheduling. *)
-Require Export rt.model.basic.task_arrival.
\ No newline at end of file
diff --git a/model/apa/time.v b/model/apa/time.v
deleted file mode 100644
index 394817a0f5a1deef15d9e34ac23dea748feec9ec..0000000000000000000000000000000000000000
--- a/model/apa/time.v
+++ /dev/null
@@ -1,2 +0,0 @@
-(* The definition of time is the same. *)
-Require Export rt.model.basic.time.
\ No newline at end of file
diff --git a/model/apa/workload.v b/model/apa/workload.v
deleted file mode 100644
index b3482234eedcb5ac8bd3676ff5a7156d51b60d5d..0000000000000000000000000000000000000000
--- a/model/apa/workload.v
+++ /dev/null
@@ -1,2 +0,0 @@
-(* The definition of workload does not change under APA scheduling. *)
-Require Export rt.model.basic.workload.
\ No newline at end of file
diff --git a/model/basic/arrival_sequence.v b/model/arrival_sequence.v
similarity index 98%
rename from model/basic/arrival_sequence.v
rename to model/arrival_sequence.v
index dcb43d3871917ce82bac107882457d2f2d8b2e20..a38e3ea8c70a819239e1ebb6a367f37a914b987d 100644
--- a/model/basic/arrival_sequence.v
+++ b/model/arrival_sequence.v
@@ -1,4 +1,4 @@
-Require Import rt.util.all rt.model.basic.task rt.model.basic.time.
+Require Import rt.util.all rt.model.task rt.model.time.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
 (* Definitions and properties of job arrival sequences. *)
diff --git a/model/basic/constrained_deadlines.v b/model/global/basic/constrained_deadlines.v
similarity index 98%
rename from model/basic/constrained_deadlines.v
rename to model/global/basic/constrained_deadlines.v
index 04d6105d588574118f9915440a1becc7fbe5a2c1..30b843df3680bb4f20bd2d367bf10cdd670078f6 100644
--- a/model/basic/constrained_deadlines.v
+++ b/model/global/basic/constrained_deadlines.v
@@ -1,7 +1,7 @@
 Require Import rt.util.all.
-Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.schedule
-               rt.model.basic.priority rt.model.basic.task_arrival
-               rt.model.basic.interference rt.model.basic.platform.
+Require Import rt.model.task rt.model.job rt.model.priority rt.model.task_arrival.
+Require Import rt.model.global.basic.schedule rt.model.global.basic.interference
+               rt.model.global.basic.platform.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
 Module ConstrainedDeadlines.
diff --git a/model/basic/interference.v b/model/global/basic/interference.v
similarity index 84%
rename from model/basic/interference.v
rename to model/global/basic/interference.v
index b1d1031be6dcf2125c03b11d3cbad1d344f592fd..6998812ec43694b195c02c991acb634312d008cd 100644
--- a/model/basic/interference.v
+++ b/model/global/basic/interference.v
@@ -1,55 +1,13 @@
 Require Import rt.util.all.
-Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.schedule
-               rt.model.basic.priority rt.model.basic.workload.
+Require Import rt.model.task rt.model.job rt.model.priority.
+Require Import rt.model.global.workload.
+Require Import rt.model.global.basic.schedule.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 Module Interference.
 
   Import Schedule ScheduleOfSporadicTask Priority Workload.
 
-  (* In this section, we define the notion of a possible interfering task. *)
-  Section PossibleInterferingTasks.
-
-    Context {sporadic_task: eqType}.
-    Variable task_cost: sporadic_task -> time.
-    Variable task_period: sporadic_task -> time.
-    Variable task_deadline: sporadic_task -> time.
-
-    Section FP.
-
-      (* Assume an FP policy. *)
-      Variable higher_eq_priority: FP_policy sporadic_task.
-
-      (* Let tsk be the task to be analyzed ... *)
-      Variable tsk: sporadic_task.
-
-      (* ...and let tsk_other be another task. *)
-      Variable tsk_other: sporadic_task.
-
-      (* Under FP scheduling with constrained deadlines, tsk_other can only interfere
-         with tsk if it is a different task with higher priority. *)
-      Definition higher_priority_task :=
-        higher_eq_priority tsk_other tsk &&
-        (tsk_other != tsk).
-
-    End FP.
-
-    Section JLFP.
-
-      (* Let tsk be the task to be analyzed ... *)
-      Variable tsk: sporadic_task.
-
-      (* ...and let tsk_other be another task. *)
-      Variable tsk_other: sporadic_task.
-
-      (* Under JLFP/JLDP scheduling with constrained deadlines, tsk_other can only interfere
-         with tsk if it is a different task. *)
-      Definition different_task := tsk_other != tsk.
-
-    End JLFP.
-    
-  End PossibleInterferingTasks.
-  
   Section InterferenceDefs.
 
     Context {sporadic_task: eqType}.
diff --git a/model/basic/interference_edf.v b/model/global/basic/interference_edf.v
similarity index 91%
rename from model/basic/interference_edf.v
rename to model/global/basic/interference_edf.v
index 1058ed3ed750be87988a614fc2ee721c1f62409f..7ff6c14e6fe6a3a94c321a909f03b15acc6b818c 100644
--- a/model/basic/interference_edf.v
+++ b/model/global/basic/interference_edf.v
@@ -1,7 +1,7 @@
 Require Import rt.util.all.
-Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.schedule
-               rt.model.basic.priority rt.model.basic.task_arrival rt.model.basic.interference
-               rt.model.basic.arrival_sequence rt.model.basic.platform.
+Require Import rt.model.task rt.model.job rt.model.priority rt.model.task_arrival.
+Require Import rt.model.global.basic.schedule rt.model.global.basic.interference
+               rt.model.global.basic.platform.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
 Module InterferenceEDF.
diff --git a/model/basic/platform.v b/model/global/basic/platform.v
similarity index 97%
rename from model/basic/platform.v
rename to model/global/basic/platform.v
index d7e31764f77f5bf1f974b71113cff6bc0c7f1386..77c7757d7027e926ebf5e746a82197dd0ba8f43a 100644
--- a/model/basic/platform.v
+++ b/model/global/basic/platform.v
@@ -1,6 +1,6 @@
 Require Import rt.util.all.
-Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.schedule
-               rt.model.basic.priority rt.model.basic.task_arrival rt.model.basic.interference.
+Require Import rt.model.task rt.model.job rt.model.priority rt.model.task_arrival.
+Require Import rt.model.global.basic.schedule rt.model.global.basic.interference.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
 Module Platform.
diff --git a/model/basic/schedule.v b/model/global/basic/schedule.v
similarity index 99%
rename from model/basic/schedule.v
rename to model/global/basic/schedule.v
index 59a423fb2082874db98d926cb8bc643d814d253f..838e491ada6278813346eabbf90694dd5aef4acf 100644
--- a/model/basic/schedule.v
+++ b/model/global/basic/schedule.v
@@ -1,5 +1,5 @@
 Require Import rt.util.all
-               rt.model.basic.job rt.model.basic.task rt.model.basic.arrival_sequence.
+               rt.model.job rt.model.task rt.model.arrival_sequence.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 (* Definition, properties and lemmas about schedules. *)
diff --git a/model/jitter/constrained_deadlines.v b/model/global/jitter/constrained_deadlines.v
similarity index 98%
rename from model/jitter/constrained_deadlines.v
rename to model/global/jitter/constrained_deadlines.v
index 807164d5f742e4380e40abeb5831c037a691ee20..33f5977edf7a4e379f0e8f766e18d1c044eff936 100644
--- a/model/jitter/constrained_deadlines.v
+++ b/model/global/jitter/constrained_deadlines.v
@@ -1,7 +1,7 @@
 Require Import rt.util.all.
-Require Import rt.model.jitter.task rt.model.jitter.job rt.model.jitter.schedule
-               rt.model.jitter.priority rt.model.jitter.task_arrival
-               rt.model.jitter.interference rt.model.jitter.platform.
+Require Import rt.model.task rt.model.priority rt.model.task_arrival.
+Require Import rt.model.global.jitter.job rt.model.global.jitter.schedule
+               rt.model.global.jitter.interference rt.model.global.jitter.platform.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
 Module ConstrainedDeadlines.
diff --git a/model/jitter/interference.v b/model/global/jitter/interference.v
similarity index 97%
rename from model/jitter/interference.v
rename to model/global/jitter/interference.v
index f6ee8eed753bbd64ce44462c9a5e6388345a13e6..0afd8a122e0ac0f2b0e8dae41b5e1b46b14cd28d 100644
--- a/model/jitter/interference.v
+++ b/model/global/jitter/interference.v
@@ -1,7 +1,6 @@
-
 Require Import rt.util.all.
-Require Import rt.model.jitter.task rt.model.jitter.job rt.model.jitter.schedule
-               rt.model.jitter.priority rt.model.jitter.workload.
+Require Import rt.model.task rt.model.priority rt.model.global.workload.
+Require Import rt.model.global.jitter.job rt.model.global.jitter.schedule.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 Module Interference.
@@ -11,7 +10,7 @@ Module Interference.
   (* We import some of the basic definitions, but we need to re-define almost everything
      since the definition of backlogged (and thus the definition of interference)
      changes with jitter. *)
-  Require Import rt.model.basic.interference.
+  Require Import rt.model.global.basic.interference.
   Export Interference.
   
   Section InterferenceDefs.
diff --git a/model/jitter/interference_edf.v b/model/global/jitter/interference_edf.v
similarity index 90%
rename from model/jitter/interference_edf.v
rename to model/global/jitter/interference_edf.v
index 6a9d4d1e2ac6358e3ef2edf5d300c4fef08b3231..09ada9aa7415be2cd9c8d67e52dcc590f2195a1a 100644
--- a/model/jitter/interference_edf.v
+++ b/model/global/jitter/interference_edf.v
@@ -1,7 +1,9 @@
 Require Import rt.util.all.
-Require Import rt.model.jitter.task rt.model.jitter.job rt.model.jitter.schedule
-               rt.model.jitter.priority rt.model.jitter.task_arrival rt.model.jitter.interference
-               rt.model.jitter.arrival_sequence rt.model.jitter.platform.
+Require Import rt.model.task rt.model.arrival_sequence rt.model.priority rt.model.task_arrival.
+Require Import rt.model.global.jitter.job
+               rt.model.global.jitter.schedule
+               rt.model.global.jitter.interference
+               rt.model.global.jitter.platform.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
 Module InterferenceEDF.
diff --git a/model/jitter/job.v b/model/global/jitter/job.v
similarity index 92%
rename from model/jitter/job.v
rename to model/global/jitter/job.v
index 35e395f385918a895c36189c81207b6935823538..2771fe8bc241275609f468965f3cf62022294427 100644
--- a/model/jitter/job.v
+++ b/model/global/jitter/job.v
@@ -1,7 +1,7 @@
-Require Import rt.model.jitter.time rt.model.jitter.task.
+Require Import rt.model.time rt.model.task.
 From mathcomp Require Import ssrnat ssrbool eqtype.  
 
-Require Export rt.model.basic.job.
+Require Export rt.model.job.
 
 (* Properties of different types of job: *)
 Module JobWithJitter.
diff --git a/model/jitter/platform.v b/model/global/jitter/platform.v
similarity index 97%
rename from model/jitter/platform.v
rename to model/global/jitter/platform.v
index cb916f90809d4cb0f54a88461af86936c0bf55bc..bd8c4a18b4c806bb68b9aa6ccae3f501c16fd1bc 100644
--- a/model/jitter/platform.v
+++ b/model/global/jitter/platform.v
@@ -1,6 +1,7 @@
 Require Import rt.util.all.
-Require Import rt.model.jitter.task rt.model.jitter.job rt.model.jitter.schedule
-               rt.model.jitter.priority rt.model.jitter.task_arrival rt.model.jitter.interference.
+Require Import rt.model.task rt.model.priority rt.model.task_arrival.
+Require Import rt.model.global.jitter.job rt.model.global.jitter.schedule
+               rt.model.global.jitter.interference.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
 Module Platform.
diff --git a/model/jitter/schedule.v b/model/global/jitter/schedule.v
similarity index 98%
rename from model/jitter/schedule.v
rename to model/global/jitter/schedule.v
index fdb9016714391c3cb6d65981d98d4cb1d0c78139..0a59571dbc8a2d61013f758e8b787776453c9ed2 100644
--- a/model/jitter/schedule.v
+++ b/model/global/jitter/schedule.v
@@ -1,12 +1,13 @@
 Require Import rt.util.all.
-Require Import rt.model.jitter.job rt.model.jitter.task rt.model.jitter.arrival_sequence.
+Require Import rt.model.task.
+Require Import rt.model.global.jitter.job rt.model.arrival_sequence.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 (* Definition, properties and lemmas about schedules. *)
 Module ScheduleWithJitter.
 
   (* We import the original schedule module and redefine whatever is required. *)
-  Require Export rt.model.basic.schedule.
+  Require Export rt.model.global.basic.schedule.
   Export ArrivalSequence Schedule.
   
   (* We need to redefine the properties of a job that depend on the arrival time. *)
diff --git a/model/basic/response_time.v b/model/global/response_time.v
similarity index 97%
rename from model/basic/response_time.v
rename to model/global/response_time.v
index 68fd3a16d5ea435730189bc56b354e8278da1b02..f8735ef719bd699d3310b246677bb9d4813e1f12 100644
--- a/model/basic/response_time.v
+++ b/model/global/response_time.v
@@ -1,6 +1,6 @@
 Require Import rt.util.all.
-Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.task_arrival
-               rt.model.basic.schedule.
+Require Import rt.model.task rt.model.job rt.model.task_arrival.
+Require Import rt.model.global.basic.schedule.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 (* Definition of response-time bound and some simple lemmas. *)
diff --git a/model/basic/schedulability.v b/model/global/schedulability.v
similarity index 98%
rename from model/basic/schedulability.v
rename to model/global/schedulability.v
index 88bdb99d3b43854356a6c419acad48e6e47e2318..69255dce87a60e57c2e7d2467c1bf05cb576c384 100644
--- a/model/basic/schedulability.v
+++ b/model/global/schedulability.v
@@ -1,5 +1,6 @@
 Require Import rt.util.all.
-Require Import rt.model.basic.job rt.model.basic.task rt.model.basic.schedule.
+Require Import rt.model.job rt.model.task.
+Require Import rt.model.global.basic.schedule.
 From mathcomp Require Import ssreflect eqtype ssrbool ssrnat seq bigop.
 
 (* Definitions of deadline miss. *)
diff --git a/model/basic/workload.v b/model/global/workload.v
similarity index 94%
rename from model/basic/workload.v
rename to model/global/workload.v
index 78f8f1a60cb4d494ea99aec7c87a32ab6635d148..b762d8d7d9951b6195e885f94970452d0b92f03c 100644
--- a/model/basic/workload.v
+++ b/model/global/workload.v
@@ -1,7 +1,7 @@
 Require Import rt.util.all.
-Require Import rt.model.basic.job rt.model.basic.task rt.model.basic.schedule
-               rt.model.basic.task_arrival rt.model.basic.response_time
-               rt.model.basic.schedulability.
+Require Import rt.model.job rt.model.task rt.model.task_arrival.
+Require Import rt.model.global.schedulability rt.model.global.response_time.
+Require Import rt.model.global.basic.schedule.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq div fintype bigop path.
 
 Module Workload.
diff --git a/model/jitter/arrival_sequence.v b/model/jitter/arrival_sequence.v
deleted file mode 100644
index 316a75b8a6796c29c6aa5f64e58d34b07c0a8272..0000000000000000000000000000000000000000
--- a/model/jitter/arrival_sequence.v
+++ /dev/null
@@ -1,3 +0,0 @@
-
-(* All definitions from arrival sequence can be safely imported. *)
-Require Export rt.model.basic.arrival_sequence.
\ No newline at end of file
diff --git a/model/jitter/priority.v b/model/jitter/priority.v
deleted file mode 100644
index 1a59a29edafce6aaebc7a3beddd74ade26f6def6..0000000000000000000000000000000000000000
--- a/model/jitter/priority.v
+++ /dev/null
@@ -1,3 +0,0 @@
-
-(* Because we define EDF using the *actual job arrivals*, we can safely import the original of priority. *)
-Require Export rt.model.basic.priority.
\ No newline at end of file
diff --git a/model/jitter/response_time.v b/model/jitter/response_time.v
deleted file mode 100644
index 673085f1b3bd8d6cb4d2b8e140bfd31dba564a76..0000000000000000000000000000000000000000
--- a/model/jitter/response_time.v
+++ /dev/null
@@ -1,4 +0,0 @@
-
-(* Since jitter does not change the notion of response time, we keep
-   the original definitions. *)
-Require Export rt.model.basic.response_time.
\ No newline at end of file
diff --git a/model/jitter/schedulability.v b/model/jitter/schedulability.v
deleted file mode 100644
index 7dfa86aff7d53b4d13f65d3892d07c3537c798ee..0000000000000000000000000000000000000000
--- a/model/jitter/schedulability.v
+++ /dev/null
@@ -1,4 +0,0 @@
-
-(* Jitter doesn't affect the notion of deadline miss, so we can safely
-   import the basic definitions. *)
-Require Export rt.model.basic.schedulability.
\ No newline at end of file
diff --git a/model/jitter/task.v b/model/jitter/task.v
deleted file mode 100644
index 73037fe62d05e1bad39faa106a7280ba9fc9b2b9..0000000000000000000000000000000000000000
--- a/model/jitter/task.v
+++ /dev/null
@@ -1,4 +0,0 @@
-
-(* Since the worst-case jitter of a task is unbounded, we don't need to
-   define any specific properties for a task with jitter.*)
-Require Export rt.model.basic.task.
\ No newline at end of file
diff --git a/model/jitter/task_arrival.v b/model/jitter/task_arrival.v
deleted file mode 100644
index d2db320ed8dc63fe098582e2b92df063e624b6a3..0000000000000000000000000000000000000000
--- a/model/jitter/task_arrival.v
+++ /dev/null
@@ -1,4 +0,0 @@
-
-(* Interarrival times are specified by the environment and are based on the
-   original arrival times. We can import the original definitions. *)
-Require Export rt.model.basic.task_arrival.
\ No newline at end of file
diff --git a/model/jitter/time.v b/model/jitter/time.v
deleted file mode 100644
index 06ad193b5fb228c7d2d6cc05aad597669eb2ab1d..0000000000000000000000000000000000000000
--- a/model/jitter/time.v
+++ /dev/null
@@ -1,3 +0,0 @@
-
-(* The definition of time is the same. *)
-Require Export rt.model.basic.time.
\ No newline at end of file
diff --git a/model/jitter/workload.v b/model/jitter/workload.v
deleted file mode 100644
index 280cc69ebcb55ec9c71d1245988e9c433fefc734..0000000000000000000000000000000000000000
--- a/model/jitter/workload.v
+++ /dev/null
@@ -1,3 +0,0 @@
-
-(* The workload of a task doesn't depend on jitter, so we keep the original definitions. *)
-Require Export rt.model.basic.workload.
\ No newline at end of file
diff --git a/model/basic/job.v b/model/job.v
similarity index 97%
rename from model/basic/job.v
rename to model/job.v
index f2fa9885261e5dfc4bdf46b1f260150f90273a52..db9227f60db5f986ae6bb9bb48117926df2ea867 100644
--- a/model/basic/job.v
+++ b/model/job.v
@@ -1,4 +1,4 @@
-Require Import rt.model.basic.time rt.model.basic.task.
+Require Import rt.model.time rt.model.task.
 From mathcomp Require Import ssrnat ssrbool eqtype.  
 
 (* Properties of different types of job: *)
diff --git a/model/basic/jobin_eqdec.v b/model/jobin_eqdec.v
similarity index 100%
rename from model/basic/jobin_eqdec.v
rename to model/jobin_eqdec.v
diff --git a/model/basic/priority.v b/model/priority.v
similarity index 83%
rename from model/basic/priority.v
rename to model/priority.v
index f2898b5181c5e023ea646d48cb8a5ac37cc7062e..9dc73ad24f2191a1de8ce17788c9cb2de68fe115 100644
--- a/model/basic/priority.v
+++ b/model/priority.v
@@ -1,12 +1,12 @@
 Require Import rt.util.all.
-Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.schedule.
+Require Import rt.model.task rt.model.job rt.model.arrival_sequence.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq.
 Set Implicit Arguments.
 
 (* Definitions of FP and JLFP/JLDP priority relations. *)
 Module Priority.
 
-  Import SporadicTaskset Schedule.
+  Import SporadicTaskset ArrivalSequence.
 
   Section PriorityDefs.
 
@@ -247,4 +247,47 @@ Module Priority.
 
   End KnownJLFPPolicies.
 
+  (* In this section, we define the notion of a possible interfering task. *)
+  Section PossibleInterferingTasks.
+
+    Context {sporadic_task: eqType}.
+    Variable task_cost: sporadic_task -> time.
+    Variable task_period: sporadic_task -> time.
+    Variable task_deadline: sporadic_task -> time.
+
+    Section FP.
+
+      (* Assume an FP policy. *)
+      Variable higher_eq_priority: FP_policy sporadic_task.
+
+      (* Let tsk be the task to be analyzed ... *)
+      Variable tsk: sporadic_task.
+
+      (* ...and let tsk_other be another task. *)
+      Variable tsk_other: sporadic_task.
+
+      (* Under FP scheduling with constrained deadlines, tsk_other can only interfere
+         with tsk if it is a different task with higher priority. *)
+      Definition higher_priority_task :=
+        higher_eq_priority tsk_other tsk &&
+        (tsk_other != tsk).
+
+    End FP.
+
+    Section JLFP.
+
+      (* Let tsk be the task to be analyzed ... *)
+      Variable tsk: sporadic_task.
+
+      (* ...and let tsk_other be another task. *)
+      Variable tsk_other: sporadic_task.
+
+      (* Under JLFP/JLDP scheduling with constrained deadlines, tsk_other can only interfere
+         with tsk if it is a different task. *)
+      Definition different_task := tsk_other != tsk.
+
+    End JLFP.
+    
+  End PossibleInterferingTasks.  
+
 End Priority.
\ No newline at end of file
diff --git a/model/basic/task.v b/model/task.v
similarity index 98%
rename from model/basic/task.v
rename to model/task.v
index f6c3f0d85476e414753236f43d63f5b3cc6cf934..6dee9d6a852e5f6a474a12951904ff3e34686524 100644
--- a/model/basic/task.v
+++ b/model/task.v
@@ -1,4 +1,4 @@
-Require Import rt.model.basic.time rt.util.all.
+Require Import rt.model.time rt.util.all.
 From mathcomp Require Import ssrnat ssrbool eqtype fintype seq.
 
 (* Attributes of a valid sporadic task. *)
diff --git a/model/basic/task_arrival.v b/model/task_arrival.v
similarity index 90%
rename from model/basic/task_arrival.v
rename to model/task_arrival.v
index 44a769db2d57c7f640a4f86e57aa8bd0242f3351..e65ff3794737c598f67ac524b78c61e7b0029b69 100644
--- a/model/basic/task_arrival.v
+++ b/model/task_arrival.v
@@ -1,11 +1,11 @@
 Require Import rt.util.all.
-Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.schedule.
+Require Import rt.model.arrival_sequence rt.model.task rt.model.job.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq.
 
 (* Properties of the job arrival. *)
 Module SporadicTaskArrival.
 
-Import SporadicTaskset Schedule.
+Import ArrivalSequence SporadicTaskset.
   
   Section ArrivalModels.
 
diff --git a/model/basic/time.v b/model/time.v
similarity index 100%
rename from model/basic/time.v
rename to model/time.v