diff --git a/analysis/facts/model/ideal_uni_exceed.v b/analysis/facts/model/ideal_uni_exceed.v
new file mode 100644
index 0000000000000000000000000000000000000000..d8fd41ec4a01e40f40a13cd3a3678a6710d21f32
--- /dev/null
+++ b/analysis/facts/model/ideal_uni_exceed.v
@@ -0,0 +1,116 @@
+Require Import prosa.model.processor.ideal_uni_exceed.
+Require Export prosa.model.processor.platform_properties.
+
+(** In the following section, we prove some general properties about the
+ ideal uniprocessor with exceedance processor state. *)
+Section ExceedanceProcStateProperties.
+
+ (** In this section, we consider any type of jobs. *)
+ Context `{Job : JobType}.
+
+ (** First we prove that the processor state provides unit supply. *)
+ Lemma eps_is_unit_supply : unit_supply_proc_model (exceedance_proc_state Job).
+ Proof.
+ rewrite /unit_supply_proc_model.
+ move => s.
+ destruct s => //=.
+ all : by rewrite /supply_in //=;rewrite sum_unit1.
+ Qed.
+
+ (** The usually opaque predicates are made transparent for this section
+ to enable us to prove some processor properties. *)
+ Local Transparent scheduled_in scheduled_on service_on.
+
+ (** A job [j] is said to be [scheduled_at] some time [t] if and only if the
+ processor state at that time is [NominalExecution j] or
+ [ExceedanceExecution j]. *)
+ Lemma scheduled_at_procstate (sched : schedule (exceedance_proc_state Job)) j t:
+ scheduled_at sched j t <->
+ sched t = NominalExecution j \/ sched t = ExceedanceExecution j.
+ Proof.
+ split.
+ - move => /existsP [c SCHEDON].
+ destruct (sched t); try done.
+ + by left; move : SCHEDON => /eqP <-.
+ + by right; move : SCHEDON => /eqP <-.
+ - rewrite /scheduled_at.
+ by move => [-> | -> ]; rewrite /scheduled_in /scheduled_on //=; apply /existsP.
+ Qed.
+
+
+ (** Next we prove that the processor model under consideration is a uniprocessor
+ model i.e., only one job can be scheduled at any time instant. *)
+ Lemma eps_is_uniproc : uniprocessor_model (exceedance_proc_state Job).
+ Proof.
+ move => j1 j2 sched t /existsP [? SCHED1] /existsP [? SCHED2].
+ destruct (sched t) eqn: EQ; try done.
+ - by move : SCHED1 => /eqP <-; move : SCHED2 => /eqP <-.
+ - by move : SCHED1 => /eqP <-; move : SCHED2 => /eqP <-.
+ Qed.
+
+ (** Next, we prove that the processor model under consideration is fully
+ consuming i.e., all the supply offered is consumed by the scheduled job. *)
+ Lemma eps_is_fully_consuming :
+ fully_consuming_proc_model (exceedance_proc_state Job).
+ Proof.
+ rewrite /fully_consuming_proc_model.
+ move => j sched t SCHED1.
+ rewrite /scheduled_at /scheduled_in in SCHED1.
+ apply scheduled_at_procstate in SCHED1.
+ move : SCHED1 => [SCHED1 | SCHED1].
+ - by rewrite /service_at /service_in /exceedance_service_on /supply_at /supply_in
+ !/exceedance_service_on //= SCHED1 sum_unit1 // sum_unit1 //
+ /exceedance_service_on /exceedance_supply_on eq_refl.
+ - by rewrite /service_at /service_in /exceedance_service_on /supply_at /supply_in
+ !/exceedance_service_on //= SCHED1 sum_unit1 // sum_unit1 //
+ /exceedance_service_on /exceedance_supply_on eq_refl.
+ Qed.
+
+ (** Finally we prove that the processor model under consideration is unit
+ service i.e., it provides at most one unit of service at any time instant. *)
+ Lemma eps_is_unit_service : unit_service_proc_model (exceedance_proc_state Job).
+ Proof.
+ move => j pstate.
+ rewrite /service_in /service_on //= sum_unit1 /exceedance_service_on.
+ destruct pstate =>//=.
+ by apply leq_b1.
+ Qed.
+
+End ExceedanceProcStateProperties.
+
+(** Next, we prove some general properties specific to the
+ ideal uniprocessor with exceedance processor state. *)
+Section ExceedanceProcStateProperties1.
+
+ (** In this section we consider any type of jobs. *)
+ Context `{Job : JobType}.
+
+ (** First let us define the notion of exceedance execution. A processor state
+ is said to be an exceedance execution state if is equal to
+ [ExceedanceExecution j] for some [j]. *)
+ Definition is_exceedance_exec (pstate : (exceedance_proc_state Job)) :=
+ match pstate with
+ |ExceedanceExecution _ => true
+ |_ => false
+ end.
+
+ (** Next, let us consider any schedule of the [exceedance_proc_state]. *)
+ Variable sched : schedule (exceedance_proc_state Job).
+
+ (** We prove that the schedule being in blackout at any time [t] is equivalent
+ to the processor state at [t] being an exceedance execution state. *)
+ Lemma blackout_implies_exceedance_execution t :
+ is_blackout sched t = is_exceedance_exec (sched t).
+ Proof.
+ rewrite /is_blackout /has_supply /supply_at /supply_in
+ /is_exceedance_exec //= sum_unit1 /exceedance_supply_on.
+ destruct (sched t) eqn : PSTATE; try done.
+ Qed.
+
+End ExceedanceProcStateProperties1.
+
+Global Hint Resolve
+ eps_is_uniproc
+ eps_is_unit_supply
+ eps_is_fully_consuming
+ : basic_rt_facts.
diff --git a/model/processor/ideal_uni_exceed.v b/model/processor/ideal_uni_exceed.v
new file mode 100644
index 0000000000000000000000000000000000000000..03e30212d2cd1e8ee465c5aabfa83b0a8ce9873a
--- /dev/null
+++ b/model/processor/ideal_uni_exceed.v
@@ -0,0 +1,110 @@
+From HB Require Import structures.
+Require Export prosa.behavior.all.
+
+(** In the following, we define a processor state model for an ideal-uniprocessor
+ system with jobs possibly exhibiting exceedance. *)
+Section State.
+
+ (** For a give type of jobs ...*)
+ Context `{Job : JobType}.
+
+ (** ... the exceedance processor state is defined as follows.
+ Here, the [NominalExecution] processor state refers to the state of the
+ processor when it is executing some job [j]. [ExceedanceExecution] also
+ refers to the state of the processor when a job is executing in addition
+ to its nominal execution time. Finally, [Idle] refers to the state of the
+ processor when no job is executing. *)
+ Inductive exceedance_processor_state :=
+ | NominalExecution (j : Job)
+ | ExceedanceExecution (j : Job)
+ | Idle.
+
+ (** To efficiently use the processor state in our mechanization, we need to
+ define an [eqType] for the processor state. First, we define an inequality
+ on the processor state as follows. *)
+ Definition exceedance_processor_state_eqdef (p1 p2 : exceedance_processor_state) : bool :=
+ match p1, p2 with
+ | NominalExecution j1, NominalExecution j2 => j1 == j2
+ | ExceedanceExecution j1, ExceedanceExecution j2 => j1 == j2
+ | Idle, Idle => true
+ | _, _ => false
+ end.
+
+ (** Next, we prove that the defined notion of equality is in fact an equality. *)
+ Lemma eqn_exceedance_processor_state : Equality.axiom exceedance_processor_state_eqdef.
+ Proof.
+ unfold Equality.axiom.
+ move => s1 s2.
+ destruct (exceedance_processor_state_eqdef s1 s2) eqn: EQ.
+ - apply ReflectT.
+ by destruct s1; destruct s2 => //=; move : EQ => /eqP -> .
+ - apply /ReflectF => EQ1.
+ move : EQ => /negP. apply.
+ by destruct s1; destruct s2 => //=; inversion EQ1; subst.
+ Qed.
+
+ (** Finally, we register the processor state as an [eqType]. *)
+ HB.instance Definition _ := hasDecEq.Build exceedance_processor_state eqn_exceedance_processor_state.
+
+ (** Next, we need to define the notions of service and supply for the
+ processor state under consideration. *)
+ Section ExceedanceService.
+
+ (** Consider any job [j]. *)
+ Variable j : Job.
+
+ (** [j] is considered to be "scheduled" if the processor state is either
+ [NominalExecution j] or [ExceedanceExecution j] *)
+ Definition exceedance_scheduled_on (proc_state : exceedance_processor_state) (_ : unit)
+ : bool :=
+ match proc_state with
+ | NominalExecution j'
+ | ExceedanceExecution j' => j' == j
+ | _ => false
+ end.
+
+ (** Next, we need to define in which states the processor is offering supply.
+ This is required to specify in which states a processor can offer
+ productive work to a job. Note that when analysing a schedule of the
+ [exceedance_processor_state], we want to model all instances of
+ [ExceedanceExecution] as blackouts w.r.t. to nominal service and, therefore, the supply in this
+ processor state is defined to be [0]. *)
+ Definition exceedance_supply_on (proc_state : exceedance_processor_state)
+ (_ : unit) : work :=
+ match proc_state with
+ | NominalExecution _ => 1
+ | ExceedanceExecution _ => 0
+ | Idle => 1
+ end.
+
+ (** Finally we need to define in which states a job actually receives
+ nominal service. In our case, a job [j] receives nominal service only when the system
+ is in the [NominalExecution j] state. *)
+ Definition exceedance_service_on (proc_state : exceedance_processor_state) (_ : unit) : work :=
+ match proc_state with
+ | NominalExecution j' => j' == j
+ | ExceedanceExecution _ => 0
+ | Idle => 0
+ end.
+
+ End ExceedanceService.
+
+ (** Finally we can declare our processor state as an instance of the
+ [ProcessorState] typeclass. *)
+ Global Program Instance exceedance_proc_state : ProcessorState Job :=
+ {|
+ State := exceedance_processor_state;
+ scheduled_on := exceedance_scheduled_on;
+ supply_on := exceedance_supply_on;
+ service_on := exceedance_service_on
+ |}.
+ Next Obligation.
+ by move => j [] // s [] /=; case: eqP; lia.
+ Qed.
+ Next Obligation.
+ by move => j [] // s [] /=; case: eqP; lia.
+ Qed.
+
+End State.
+
+Global Arguments exceedance_proc_state : clear implicits.
diff --git a/scripts/wordlist.pws b/scripts/wordlist.pws
index 0d92bc2debce04c66e20d4f77184ce31b38779c2..59d771dfeb53e44f36f8e1440a7e9b2754d10416 100644
--- a/scripts/wordlist.pws
+++ b/scripts/wordlist.pws
@@ -131,3 +131,4 @@ RHS
LHS
subsequence
Baruah
+exceedance