Library prosa.classic.analysis.apa.bertogna_edf_comp

Library prosa.classic.analysis.apa.bertogna_edf_theory

Library prosa.classic.analysis.apa.bertogna_fp_comp

Library prosa.classic.analysis.apa.bertogna_fp_theory

Library prosa.classic.analysis.apa.interference_bound

Library prosa.classic.analysis.apa.interference_bound_edf

Library prosa.classic.analysis.apa.interference_bound_fp

Library prosa.classic.analysis.apa.workload_bound

Library prosa.classic.analysis.global.basic.bertogna_edf_comp

Library prosa.classic.analysis.global.basic.bertogna_edf_theory

Library prosa.classic.analysis.global.basic.bertogna_fp_comp

Library prosa.classic.analysis.global.basic.bertogna_fp_theory

Library prosa.classic.analysis.global.basic.interference_bound

Library prosa.classic.analysis.global.basic.interference_bound_edf

Library prosa.classic.analysis.global.basic.interference_bound_fp

Library prosa.classic.analysis.global.basic.workload_bound

Library prosa.classic.analysis.global.jitter.bertogna_edf_comp

Library prosa.classic.analysis.global.jitter.bertogna_edf_theory

Library prosa.classic.analysis.global.jitter.bertogna_fp_comp

Library prosa.classic.analysis.global.jitter.bertogna_fp_theory

Library prosa.classic.analysis.global.jitter.interference_bound

Library prosa.classic.analysis.global.jitter.interference_bound_edf

Library prosa.classic.analysis.global.jitter.interference_bound_fp

Library prosa.classic.analysis.global.jitter.workload_bound

Library prosa.classic.analysis.global.parallel.bertogna_edf_comp

Library prosa.classic.analysis.global.parallel.bertogna_edf_theory

Library prosa.classic.analysis.global.parallel.bertogna_fp_comp

Library prosa.classic.analysis.global.parallel.bertogna_fp_theory

Library prosa.classic.analysis.global.parallel.interference_bound

Library prosa.classic.analysis.global.parallel.interference_bound_edf

Library prosa.classic.analysis.global.parallel.interference_bound_fp

Library prosa.classic.analysis.global.parallel.workload_bound

Library prosa.classic.analysis.uni.arrival_curves.workload_bound

Library prosa.classic.analysis.uni.basic.fp_rta_comp

Library prosa.classic.analysis.uni.basic.fp_rta_theory

Library prosa.classic.analysis.uni.basic.tdma_rta_theory

Library prosa.classic.analysis.uni.basic.tdma_wcrt_analysis

Library prosa.classic.analysis.uni.basic.workload_bound_fp

Library prosa.classic.analysis.uni.jitter.fp_rta_comp

Library prosa.classic.analysis.uni.jitter.fp_rta_theory

Library prosa.classic.analysis.uni.jitter.workload_bound_fp

Library prosa.classic.analysis.uni.susp.dynamic.jitter.jitter_schedule

Library prosa.classic.analysis.uni.susp.dynamic.jitter.jitter_schedule_properties

Library prosa.classic.analysis.uni.susp.dynamic.jitter.jitter_schedule_service

• • 6-(A) Less High-Priority Service Before the Arrival of Job j in sched_jitter
    • • Main Claim of Section (A)
  • 6-(B) More High-Priority Service After the Arrival of Job j in sched_jitter
    • • Main Claim of Section (B)
  • 6-(C) Conclusion: Comparing Response Times of Job j
    • • Main Claim of Section (C)

Library prosa.classic.analysis.uni.susp.dynamic.jitter.jitter_taskset_generation

Library prosa.classic.analysis.uni.susp.dynamic.jitter.rta_by_reduction

• • • • Main Claim

Library prosa.classic.analysis.uni.susp.dynamic.jitter.taskset_membership

Library prosa.classic.analysis.uni.susp.dynamic.jitter.taskset_rta

Library prosa.classic.analysis.uni.susp.dynamic.oblivious.fp_rta

Library prosa.classic.analysis.uni.susp.dynamic.oblivious.reduction

Library prosa.classic.analysis.uni.susp.sustainability.allcosts.main_claim

Library prosa.classic.analysis.uni.susp.sustainability.allcosts.reduction

Library prosa.classic.analysis.uni.susp.sustainability.allcosts.reduction_properties

Library prosa.classic.analysis.uni.susp.sustainability.singlecost.reduction

Library prosa.classic.analysis.uni.susp.sustainability.singlecost.reduction_properties

Library prosa.classic.implementation.apa.arrival_sequence

Library prosa.classic.implementation.apa.bertogna_edf_example

Library prosa.classic.implementation.apa.bertogna_fp_example

Library prosa.classic.implementation.apa.job

Library prosa.classic.implementation.apa.schedule

Library prosa.classic.implementation.apa.task

Library prosa.classic.implementation.arrival_sequence

Library prosa.classic.implementation.global.basic.bertogna_edf_example

Library prosa.classic.implementation.global.basic.bertogna_fp_example

Library prosa.classic.implementation.global.basic.schedule

Library prosa.classic.implementation.global.jitter.arrival_sequence

Library prosa.classic.implementation.global.jitter.bertogna_edf_example

Library prosa.classic.implementation.global.jitter.bertogna_fp_example

Library prosa.classic.implementation.global.jitter.job

Library prosa.classic.implementation.global.jitter.schedule

Library prosa.classic.implementation.global.jitter.task

Library prosa.classic.implementation.global.parallel.bertogna_edf_example

Library prosa.classic.implementation.global.parallel.bertogna_fp_example

Library prosa.classic.implementation.job

Library prosa.classic.implementation.task

Library prosa.classic.implementation.uni.basic.extraction_tdma

Library prosa.classic.implementation.uni.basic.fp_rta_example

Library prosa.classic.implementation.uni.basic.schedule

Library prosa.classic.implementation.uni.basic.schedule_tdma

Library prosa.classic.implementation.uni.basic.tdma_rta_example

Library prosa.classic.implementation.uni.jitter.arrival_sequence

Library prosa.classic.implementation.uni.jitter.fp_rta_example

Library prosa.classic.implementation.uni.jitter.job

Library prosa.classic.implementation.uni.jitter.schedule

Library prosa.classic.implementation.uni.jitter.task

Library prosa.classic.implementation.uni.susp.dynamic.arrival_sequence

Library prosa.classic.implementation.uni.susp.dynamic.job

Library prosa.classic.implementation.uni.susp.dynamic.oblivious.fp_rta_example

Library prosa.classic.implementation.uni.susp.dynamic.task

Library prosa.classic.implementation.uni.susp.schedule

Library prosa.classic.model.arrival.basic.arrival_bounds

Library prosa.classic.model.arrival.basic.arrival_sequence

Library prosa.classic.model.arrival.basic.job

Library prosa.classic.model.arrival.basic.task

Library prosa.classic.model.arrival.basic.task_arrival

Library prosa.classic.model.arrival.curves.bounds

Library prosa.classic.model.arrival.jitter.arrival_bounds

Library prosa.classic.model.arrival.jitter.arrival_sequence

Library prosa.classic.model.arrival.jitter.job

Library prosa.classic.model.arrival.jitter.task_arrival

Library prosa.classic.model.policy_tdma

Library prosa.classic.model.priority

Library prosa.classic.model.schedule.apa.affinity

Library prosa.classic.model.schedule.apa.constrained_deadlines

Library prosa.classic.model.schedule.apa.interference

Library prosa.classic.model.schedule.apa.interference_edf

Library prosa.classic.model.schedule.apa.platform

Library prosa.classic.model.schedule.global.basic.constrained_deadlines

Library prosa.classic.model.schedule.global.basic.interference

Library prosa.classic.model.schedule.global.basic.interference_edf

Library prosa.classic.model.schedule.global.basic.platform

Library prosa.classic.model.schedule.global.basic.schedule

Library prosa.classic.model.schedule.global.jitter.constrained_deadlines

Library prosa.classic.model.schedule.global.jitter.interference

Library prosa.classic.model.schedule.global.jitter.interference_edf

Library prosa.classic.model.schedule.global.jitter.job

Library prosa.classic.model.schedule.global.jitter.platform

Library prosa.classic.model.schedule.global.jitter.schedule

Library prosa.classic.model.schedule.global.response_time

Library prosa.classic.model.schedule.global.schedulability

Library prosa.classic.model.schedule.global.transformation.construction

Library prosa.classic.model.schedule.global.workload

Library prosa.classic.model.schedule.partitioned.schedulability

Library prosa.classic.model.schedule.partitioned.schedule

Library prosa.classic.model.schedule.uni.basic.platform

Library prosa.classic.model.schedule.uni.basic.platform_tdma

Library prosa.classic.model.schedule.uni.end_time

Library prosa.classic.model.schedule.uni.jitter.busy_interval

Library prosa.classic.model.schedule.uni.jitter.platform

Library prosa.classic.model.schedule.uni.jitter.schedule

Library prosa.classic.model.schedule.uni.jitter.valid_schedule

Library prosa.classic.model.schedule.uni.limited.abstract_RTA.abstract_rta

• Abstract Response-Time Analysis

Library prosa.classic.model.schedule.uni.limited.abstract_RTA.abstract_seq_rta

• Abstract Response-Time Analysis with sequential jobs

Library prosa.classic.model.schedule.uni.limited.abstract_RTA.definitions

• Definitions for Abstract Response-Time Analysis

Library prosa.classic.model.schedule.uni.limited.abstract_RTA.reduction_of_search_space

• Reduction of the serach space for Abstract RTA

Library prosa.classic.model.schedule.uni.limited.abstract_RTA.sufficient_condition_for_lock_in_service

• Lock-in service of a job

Library prosa.classic.model.schedule.uni.limited.busy_interval

• Busy Interval for JLFP-models

Library prosa.classic.model.schedule.uni.limited.edf.nonpr_reg.concrete_models.response_time_bound

• RTA for concrete models
• RTA for fully preemptive EDF model
• RTA for fully nonpreemptive EDF model
• RTA for EDF with fixed premption points
• RTA for EDF with floating nonpreemptive regions

Library prosa.classic.model.schedule.uni.limited.edf.nonpr_reg.response_time_bound

• RTA for EDF-schedulers with bounded nonpreemprive segments
  • Priority inversion is bounded
  • Response-Time Bound

Library prosa.classic.model.schedule.uni.limited.edf.response_time_bound

• Abstract RTA for EDF-schedulers
  • Filling Out Hypothesis Of Abstract RTA Theorem
  • Final Theorem

Library prosa.classic.model.schedule.uni.limited.fixed_priority.nonpr_reg.concrete_models.response_time_bound

• RTA for concrete models
• RTA for fully preemptive FP model
• RTA for fully nonpreemptive FP model
• RTA for FP-schedulers with fixed premption points
• RTA for FP-schedulers with floating nonpreemptive regions

Library prosa.classic.model.schedule.uni.limited.fixed_priority.nonpr_reg.response_time_bound

• RTA for FP-schedulers with bounded nonpreemptive segments
  • Priority inversion is bounded
  • Response-Time Bound

Library prosa.classic.model.schedule.uni.limited.fixed_priority.response_time_bound

• Abstract RTA for FP-schedulers
  • Filling Out Hypotheses Of Abstract RTA Theorem
  • Final Theorem

Library prosa.classic.model.schedule.uni.limited.jlfp_instantiation

• JLFP instantiation of Interference and Interfering Workload
  • Interference and Interfering Workload
  • Equivalences

Library prosa.classic.model.schedule.uni.limited.platform.definitions

• Platform with limited preemptions

Library prosa.classic.model.schedule.uni.limited.platform.limited

• Platform for models with limited preemptions

Library prosa.classic.model.schedule.uni.limited.platform.nonpreemptive

• Platform for fully nonpreemptive model

Library prosa.classic.model.schedule.uni.limited.platform.preemptive

• Platform for fully premptive model

Library prosa.classic.model.schedule.uni.limited.platform.priority_inversion_is_bounded

• Priority inversion is bounded

Library prosa.classic.model.schedule.uni.limited.rbf

Library prosa.classic.model.schedule.uni.limited.schedule

Library prosa.classic.model.schedule.uni.nonpreemptive.platform

Library prosa.classic.model.schedule.uni.nonpreemptive.schedule

Library prosa.classic.model.schedule.uni.response_time

Library prosa.classic.model.schedule.uni.schedulability

Library prosa.classic.model.schedule.uni.schedule

Library prosa.classic.model.schedule.uni.schedule_of_task

Library prosa.classic.model.schedule.uni.service

Library prosa.classic.model.schedule.uni.susp.build_suspension_table

Library prosa.classic.model.schedule.uni.susp.last_execution

Library prosa.classic.model.schedule.uni.susp.platform

Library prosa.classic.model.schedule.uni.susp.schedule

Library prosa.classic.model.schedule.uni.susp.suspension_intervals

Library prosa.classic.model.schedule.uni.susp.valid_schedule

Library prosa.classic.model.schedule.uni.sustainability

Library prosa.classic.model.schedule.uni.transformation.construction

Library prosa.classic.model.schedule.uni.workload

Library prosa.classic.model.suspension

Library prosa.classic.model.time

Library prosa.classic.util.all

Library prosa.classic.util.bigcat

Library prosa.classic.util.bigord

Library prosa.classic.util.counting

Library prosa.classic.util.div_mod

Library prosa.classic.util.find_seq

Library prosa.classic.util.fixedpoint

Library prosa.classic.util.induction

Library prosa.classic.util.list

Library prosa.classic.util.minmax

Library prosa.classic.util.nat

Library prosa.classic.util.notation

Library prosa.classic.util.ord_quantifier

Library prosa.classic.util.pick

Library prosa.classic.util.powerset

Library prosa.classic.util.seqset

Library prosa.classic.util.sorting

• Sorting

Library prosa.classic.util.step_function

Library prosa.classic.util.sum

Library prosa.classic.util.tactics

• Very basic automation
• Equality types
• Basic simplification tactics
  • Delineating cases in proofs
• New tactics for ssreflect

Library prosa.util.all

Library prosa.util.bigcat

Library prosa.util.div_mod

Library prosa.util.epsilon

Library prosa.util.fixpoint

• Fixpoint Search
  • Least Positive Fixpoint
  • Maximal Fixpoint across a Search Space
  • Search Space Defined by a Predicate

Library prosa.util.lcmseq

Library prosa.util.list

Library prosa.util.minmax

Library prosa.util.nat

Library prosa.util.nondecreasing

• Non-Decreasing Sequence and Distances
• Properties of Increasing Sequence
• Properties of Non-Decreasing Sequence
• Properties of Undup of Non-Decreasing Sequence
• Properties of Distances
• Properties of Distances of Non-Decreasing Sequence

Library prosa.util.notation

Library prosa.util.rel

Library prosa.util.search_arg

Library prosa.util.seqset

Library prosa.util.setoid

Library prosa.util.subadditivity

Library prosa.util.sum

Library prosa.util.superadditivity

Library prosa.util.supremum

• Computation of a Sequence's Supremum

Library prosa.util.tactics

• • Exploiting a hypothesis
• Handier movement of inequalities.

Library prosa.util.unit_growth