rt.model.time: Definition of time.rt.model.priority: Definitions and lemmas about priorities.rt.model.suspension: Definition of the suspension model.rt.model.policy_tdma: Definitions related to TDMA policies.rt.model.arrival.basic.arrival_sequence: Definitions and lemmas about arrival sequences.rt.model.arrival.basic.job: Definition of a valid sporadic job.rt.model.arrival.basic.task: Definition of a valid sporadic task.rt.model.arrival.basic.task_arrival: Definition of the sporadic task model and related lemmas.rt.model.arrival.basic.arrival_bounds: Definition of the bound on the arrival of sporadic jobs with jitter.rt.model.arrival.jitter.arrival_sequence: Additional definitions about arrival sequences with jitter.rt.model.arrival.jitter.job: Definition of a valid sporadic job with jitter.rt.model.arrival.jitter.arrival_bounds: Definition of the bound on the arrival of sporadic jobs with jitter.rt.model.arrival.jitter.task_arrival: Definition of the sporadic task model for tasks with jitter.rt.model.schedule.uni.schedule: Definition and lemmas about uniprocessor schedules.rt.model.schedule.uni.service: Definitions and lemmas related to service.rt.model.schedule.uni.schedulability: Definition of deadline miss.rt.model.schedule.uni.response_time: Definitions and lemmas about response-time bounds.rt.model.schedule.uni.workload: Definitions and lemmas about workload.rt.model.schedule.uni.end_time: Definition of completion time.rt.model.schedule.uni.sustainability: Definition of weak and strong sustainability.rt.model.schedule.uni.schedule_of_task: Definitions and lemmas about schedules of sporadic tasks.rt.model.schedule.uni.transformation.construction: Prefix-based construction of a uniprocessor scheduled using a provided algorithm.rt.model.schedule.uni.basic.busy_interval: Definitions and lemmas about busy intervals.rt.model.schedule.uni.basic.platform: Definition of the platform constraints.rt.model.schedule.uni.basic.platform_tdma: Definitions related to TDMA policies.rt.model.schedule.uni.jitter.schedule: Extra definitions for schedules with jitter.rt.model.schedule.uni.jitter.valid_schedule: Definition of a valid schedule with jitter.rt.model.schedule.uni.jitter.platform: Platform constraints for schedules with jitter.rt.model.schedule.uni.jitter.busy_interval: Definitions and lemmas related to busy interval in schedules with jitter.rt.model.schedule.uni.susp.schedule: Extra definitions for schedules of self-suspending tasks.rt.model.schedule.uni.susp.valid_schedule: Notion of valid schedule with suspensions.rt.model.schedule.uni.susp.suspension_intervals: Definition of a suspension interval.rt.model.schedule.uni.susp.last_execution: Definition of the instant after the last execution of a job.rt.model.schedule.uni.susp.platform: Platform constraints for self-suspending tasks.rt.model.schedule.uni.susp.build_suspension_table: Generation of suspension tables using some predicate.rt.model.schedule.global.response_time: Definitions and lemmas about response-time bounds.rt.model.schedule.global.schedulability: Definitions and lemmas about deadline misses.rt.model.schedule.global.workload: Definitions and lemmas about workload.rt.model.schedule.global.transformation.construction: Prefix-based construction of a global schedule using a provided algorithm.rt.model.schedule.global.basic.schedule: Definitions and lemmas about schedules.rt.model.schedule.global.basic.platform: Definitions and lemmas about the processor platform.rt.model.schedule.global.basic.constrained_deadlines: Lemmas about the processor platform under constrained deadlines.rt.model.schedule.global.basic.interference: Definitions and lemmas about interference.rt.model.schedule.global.basic.interference_edf: Lemmas about interference in EDF-scheduled systems.rt.model.schedule.global.jitter.job: Extra definitions about jobs with jitter.rt.model.schedule.global.jitter.schedule: Definitions and lemmas about schedules with jitter.rt.model.schedule.global.jitter.platform: Definitions and lemmas about the processor platform.rt.model.schedule.global.jitter.interference_edf: Lemmas about interference in EDF-scheduled systems.rt.model.schedule.global.jitter.interference: Definitions and lemmas about interference.rt.model.schedule.global.jitter.constrained_deadlines: Lemmas about the processor platform under constrained deadlines.rt.model.schedule.partitioned.schedule: Definition of partitioned scheduling.rt.model.schedule.partitioned.schedulability: Definitions relating the schedulability of global and partitioned scheduling.rt.model.schedule.apa.affinity: Definition of a processor affinity.rt.model.schedule.apa.interference_edf: Lemmas about interference in EDF-scheduled systems.rt.model.schedule.apa.interference: Definitions and lemmas about interference.rt.model.schedule.apa.constrained_deadlines: Lemmas about the processor platform under constrained deadlines.rt.model.schedule.apa.platform: Definitions and lemmas about the processor platform.rt.analysis.uni.basic.workload_bound_fp: Workload bound for sporadic tasks under constrained deadlines.rt.analysis.uni.basic.fp_rta_theory: Proof that any fixed point of the FP RTA gives a response-time bound.rt.analysis.uni.basic.fp_rta_comp: Definition and proofs of correctness and termination of the RTA for sporadic tasks.rt.analysis.uni.basic.tdma_rta_theory: Proof that any fixed point of the TDMA RTA gives a response-time bound.rt.analysis.uni.basic.tdma_wcrt_analysis: Definition and proofs of correctness and termination of the RTA for TDMA tasks.rt.analysis.uni.jitter.workload_bound_fp: Workload bound for FP scheduling with constrained deadlines.rt.analysis.uni.jitter.fp_rta_theory: Proof that any fixed point of the FP RTA gives a response-time bound.rt.analysis.uni.jitter.fp_rta_comp: Definition and proofs of correctness and termination of the FP RTA.rt.analysis.uni.susp.dynamic.oblivious.reduction: Construction of a worse schedule without suspensions by inflating job costs (suspension-oblivious approach).rt.analysis.uni.susp.dynamic.oblivious.fp_rta: Instantiation of the FP RTA for self-suspending tasks based on the suspension-oblivious approach.rt.analysis.uni.susp.dynamic.jitter.jitter_schedule: Construction of the worse schedule with jitter and no suspensions (jitter-based approach).rt.analysis.uni.susp.dynamic.jitter.jitter_schedule_properties: Basic properties of the generated schedule with jitter.rt.analysis.uni.susp.dynamic.jitter.jitter_schedule_service: Service-related properties of the generated schedule with jitter.rt.analysis.uni.susp.dynamic.jitter.jitter_taskset_generation: Construction of a task set with jitter and no suspension times.rt.analysis.uni.susp.dynamic.jitter.taskset_membership: Proof that the generated task set “contains” the generated schedule.rt.analysis.uni.susp.dynamic.jitter.rta_by_reduction: Comparing response-time bounds between the original schedule (with suspensions) and the generated schedule (with jitter and no suspensions).rt.analysis.uni.susp.dynamic.jitter.taskset_rta: Using the reduction to derive a response-time analysis for the task set with suspensions.rt.analysis.global.basic.workload_bound: Definition and proof of correctness of the workload bound.rt.analysis.global.basic.interference_bound_fp: Definition of the interference bound for FP scheduling.rt.analysis.global.basic.interference_bound_edf: Definition and proof of correctness of the EDF-specific interference bound.rt.analysis.global.basic.interference_bound: Definition of the generic interference bound.rt.analysis.global.basic.bertogna_fp_theory: Proof that any fixed point in the FP RTA is a safe response-time bound.rt.analysis.global.basic.bertogna_fp_comp: Definition and proofs of correctness and termination of the FP RTA.rt.analysis.global.basic.bertogna_edf_theory: Proof that any fixed point in the EDF RTA is a safe response-time bound.rt.analysis.global.basic.bertogna_edf_comp: Definition and proofs of correctness and termination of the EDF RTA.rt.analysis.global.jitter.workload_bound: Definition and proof of correctness of the jitter-aware workload bound.rt.analysis.global.jitter.interference_bound_fp: Definition of the jitter-aware interference bound for FP scheduling.rt.analysis.global.jitter.interference_bound_edf: Definition and proof of correctness of the jitter-aware EDF-specific interference bound.rt.analysis.global.jitter.interference_bound: Definition of the generic jitter-aware interference bound.rt.analysis.global.jitter.bertogna_fp_theory: Proof that any fixed point in the jitter-aware FP RTA is a safe response-time bound.rt.analysis.global.jitter.bertogna_fp_comp: Definition and proofs of correctness and termination of the jitter-aware FP RTA.rt.analysis.global.jitter.bertogna_edf_theory: Proof that any fixed point in the jitter-aware EDF RTA is a safe response-time bound.rt.analysis.global.jitter.bertogna_edf_comp: Definition and proofs of correctness and termination of the jitter-aware EDF RTA.rt.analysis.global.parallel.workload_bound: Definition and proof of correctness of the workload bound for parallel jobs.rt.analysis.global.parallel.interference_bound: Definition of the generic interference bound for parallel jobs.rt.analysis.global.parallel.interference_bound_fp: Definition of the interference bound for FP scheduling for parallel jobs.rt.analysis.global.parallel.interference_bound_edf: Definition and proof of correctness of the EDF-specific interference bound for parallel jobs.rt.analysis.global.parallel.bertogna_fp_theory: Proof that any fixed point in the FP RTA for parallel jobs is a safe response-time bound.rt.analysis.global.parallel.bertogna_fp_comp: Definition and proofs of correctness and termination of the FP RTA for parallel jobsrt.analysis.global.parallel.bertogna_edf_theory: Proof that any fixed point in the EDF RTA for parallel jobs is a safe response-time bound.rt.analysis.global.parallel.bertogna_edf_comp: Definition and proofs of correctness and termination of the EDF RTA for parallel jobs.rt.analysis.apa.workload_bound: Definition and proof of correctness of the workload bound.rt.analysis.apa.interference_bound: Definition of the generic interference bound.rt.analysis.apa.interference_bound_fp: Definition of the interference bound for FP scheduling.rt.analysis.apa.interference_bound_edf: Definition and proof of correctness of the EDF-specific interference bound.rt.analysis.apa.bertogna_fp_theory: Proof that any fixed point in the FP RTA is a safe response-time bound.rt.analysis.apa.bertogna_fp_comp: Definition and proofs of correctness and termination of the FP RTA.rt.analysis.apa.bertogna_edf_theory: Proof that any fixed point in the EDF RTA is a safe response-time bound.rt.analysis.apa.bertogna_edf_comp: Definition and proofs of correctness and termination of the EDF RTA.rt.analysis.uni.susp.sustainability.allcosts.reduction: Construction of a schedule with worse costs and variable suspension times.rt.analysis.uni.susp.sustainability.allcosts.reduction_properties: Properties of the generated schedule with worse costs and variable suspension times.rt.analysis.uni.susp.sustainability.allcosts.main_claim: Main claim of weak-sustainability w.r.t. job costs and variable suspension times.rt.analysis.uni.susp.sustainability.singlecost.reduction: Construction of a schedule with worse costs for a single job.rt.analysis.uni.susp.sustainability.singlecost.reduction_properties: Properties of the generated schedule with worse costs for a single job.rt.implementation.arrival_sequence: Implementation of a periodic arrival sequence.rt.implementation.task: Implementation of a real-time task.rt.implementation.job: Implementation of a job.rt.implementation.uni.basic.schedule: Implementation of a work-conserving scheduler.rt.implementation.uni.basic.fp_rta_example: Example of applying the FP RTA to a concrete task set.rt.implementation.uni.basic.tdma_rta_example: Example of applying the FP RTA to a concrete task set.rt.implementation.uni.basic.schedule_tdma: Implementation of a TDMA scheduler.rt.implementation.uni.basic.extraction_tdma: Extraction of the TDMA analysis.rt.implementation.uni.jitter.job: Implementation of a job with jitter.rt.implementation.uni.jitter.task: Implementation of a real-time task with jitter.rt.implementation.uni.jitter.schedule: Implementation of a work-conserving scheduler with jitter.rt.implementation.uni.jitter.arrival_sequence: Implementation of a periodic arrival sequence.rt.implementation.uni.jitter.fp_rta_example: Example of applying the FP RTA on a concrete task set.rt.implementation.uni.susp.dynamic.job: Implementation of a job with suspensions.rt.implementation.uni.susp.dynamic.task: Implementation of a real-time task with suspensions.rt.implementation.uni.susp.dynamic.arrival_sequence: Implementation of a periodic arrival sequence.rt.implementation.uni.susp.schedule: Implementation of a work-conserving schedule with suspensions.rt.implementation.uni.susp.dynamic.oblivious.fp_rta_example: Example of applying the FP RTA on concrete self-suspending tasks.rt.implementation.global.basic.schedule: Implementation of a work-conserving scheduler.rt.implementation.global.basic.bertogna_edf_example: Example of applying the EDF RTA to a task set with 3 tasks.rt.implementation.global.basic.bertogna_fp_example: Example of applying the FP RTA to a task set with 3 tasks.rt.implementation.global.jitter.arrival_sequence: Implementation of a periodic arrival sequence for jobs with jitter.rt.implementation.global.jitter.job: Implementation of a job with jitter.rt.implementation.global.jitter.task: Implementation of a real-time task with jitter.rt.implementation.global.jitter.schedule: Implementation of a jitter-aware scheduler.rt.implementation.global.jitter.bertogna_edf_example: Example of applying the jitter-aware EDF RTA to a task set with 3 tasks.rt.implementation.global.jitter.bertogna_fp_example: Example of applying the jitter-aware FP RTA to a task set with 3 tasks.rt.implementation.global.parallel.bertogna_edf_example: Example of applying the EDF RTA for parallel jobs to a task set with 3 tasks.rt.implementation.global.parallel.bertogna_fp_example: Example of applying the FP RTA for parallel jobs to a task set with 3 tasks.rt.implementation.apa.arrival_sequence: Implementation of a periodic arrival sequence.rt.implementation.apa.job: Implementation of a job.rt.implementation.apa.schedule: Implementation of a work-conserving APA scheduler.rt.implementation.apa.task: Implementation of a real-time task with processor affinities.rt.implementation.apa.bertogna_edf_example: Example of applying the EDF RTA for parallel jobs to a task set with 3 tasks.rt.implementation.apa.bertogna_fp_example: Example of applying the FP RTA for parallel jobs to a task set with 3 tasks.rt.util.notation: Customized notations for increasing readability.rt.util.tactics: Set of tactics used in our development.rt.util.div_mod: Definitions and lemmas related to floor/ceil and division.rt.util.nat: Additional lemmas about natural numbers and arithmetic.rt.util.induction: Lemmas about induction on natural numbers.rt.util.fixedpoint: Lemmas about fixed point iterations.rt.util.ssromega: Adaptation of the Omega tactic for ssreflect.rt.util.bigcat: Lemmas about the big concatenation operator.rt.util.list: Additional lemmas about lists.rt.util.seqset: Definition of a set as a list without duplicates.rt.util.powerset: Definition and lemmas about power sets.rt.util.sorting: Additional lemmas about sorting.rt.util.bigord: Lemmas about big operators involving Ordinal functions.rt.util.ord_quantifier: Lemmas about [exists, …] and [forall, …] from ssreflect.rt.util.sum: Additional lemmas about summation.rt.util.step_function: Lemmas about step functions (e.g. service).rt.util.minmax: Definitions and lemmas about min/max.rt.util.find_seq: Definition of a find operation that can fail.rt.util.pick: Definition of pick operator for lists.rt.util.counting: Additional lemmas about counting.rt.util.all: Compilation of all utility libraries.