Library probsa.probability.brvar

• Boolean Random Variable
• Notation Instances

Library probsa.probability.cdf

Library probsa.probability.conditional

• Conditional Measure μ ↦ μ|S
• Conditional Probability and CDF
• Equivalence to Textbook Definition
• Basic Lemmas

Library probsa.probability.dominance_relation

• Instances
  • nat → R vs nat → R
  • nrvar vs nrvar
  • nrvar vs nat → R
  • rvar etime vs rvar etime

Library probsa.probability.independence

Library probsa.probability.law_of_total_prob

• Law of Total Probability

Library probsa.probability.nrvar

• Natural Random Variable
• Notation Instances

Library probsa.probability.partition

Library probsa.probability.pmf

Library probsa.probability.pred

Library probsa.probability.prob

• Additional Lemmas

Library probsa.probability.stochastic_order

Library probsa.rt.analysis.WCET_is_pWCET

• WCET is Axiomatic pWCET

Library probsa.rt.analysis.arrivals

Library probsa.rt.analysis.axiomatic_pWCET_full

• Proof of Theorem 2
  • Initial System
  • Simplified System
  • Theorem 2

Library probsa.rt.analysis.axiomatic_pWCET_step

• Step-by-step Proof of Theorem 1
  • Step 1
  • Step 2
  • Step 3
  • Step 4
  • Step 5
  • Step 6
  • Step 7
  • Step 8
  • Step 9
  • Step 10
  • Step 11
  • Step 12
  • Step 13
• Statement and Proof of Theorem 1

Library probsa.rt.analysis.completion

• Probabilistic Completion is Monotone

Library probsa.rt.analysis.completion_time

• Existence of Completion Time

Library probsa.rt.analysis.independent.cost_and_workload

Library probsa.rt.analysis.independent.task_workload

Library probsa.rt.analysis.nth_cost

Library probsa.rt.analysis.pETs_to_pWCETs

• Transformation
  • System
  • pWCET to Job Cost Random Variable
  • Replace pET of a Job
  • Replace pETs of a Set of Jobs
  • Replace pETs of All Jobs

Library probsa.rt.analysis.pRTA.pRTA

• TDFP ≤ WCA-TDFP
• TDFP Bound
• Step-by-Step Proof of Probabilistic Response-Time Analysis: TDFP Bound
  • Step-by-Step Proof Sketch
    • Step 1: Handle the case where job j doesn't arrive.
    • Step 2: Relate deadline miss to workload demand
    • Step 3: Bound workload for a single interval
    • Step 4: Bound each task's workload by a sum of job costs
    • Step 5: Bound individual job costs by pWCET
  • Main Theorem

Library probsa.rt.analysis.pRTA.pRTA_full

• Probabilistic Response-Time Analysis for Fixed-Priority Scheduling
  • Model and Assumptions
  • Main Theorem

Library probsa.rt.analysis.partition_transfer

• Partition Transfer

Library probsa.rt.analysis.scheduler_properties

• Sustainability and Properties of Fixed-Priority Fully-Preemptive Scheduling
  • Scheduler Definition and Properties
  • Verification of Scheduler Properties

Library probsa.rt.analysis.transformation_properties

• Properties of the Axiomatic-pWCET Transformation
  • Structure and Reading Guide
  • Preservation of the Sporadic Task Model
  • Preservation of the Horizon Property
  • Preservation of Arrival-Cost Consistency
  • Preservation of Arrival Sequences
  • Identical Distributions and Stochastic Bounds
  • Independence of Job Costs
  • Independence from Arrival Sequences and Conditional Independence
  • Conditional Cost Bounds

Library probsa.rt.analysis.valid_pWCET_remains_valid

• Valid pWCET Remains Valid
  • Auxiliary Lemmas
  • Valid Axiomatic pWCET Remains Valid
  • Iterative Application of Theorem 1

Library probsa.rt.analysis.work_bound

Library probsa.rt.behavior.arrival_sequence

• Probabilistic Arrival Sequence
  • job_arrival → pr_arrival_sequence for Job : Finite

Library probsa.rt.behavior.job

• Probabilistic Parameters of a Job
• Derived Notions

Library probsa.rt.behavior.response_time

• Probabilistic Response Time

Library probsa.rt.behavior.schedule

• Probabilistic Schedule

Library probsa.rt.behavior.service

• Probabilistic Service

Library probsa.rt.model.WCET

• Worst-Case Execution Time

Library probsa.rt.model.abort_readiness

Library probsa.rt.model.assumptions.basic

Library probsa.rt.model.assumptions.pr_cost

Library probsa.rt.model.assumptions.pr_must_be_ready

Library probsa.rt.model.assumptions.pr_respects_policy

Library probsa.rt.model.assumptions.pr_work_conserving

Library probsa.rt.model.axiomatic_pWCET

• Axiomatic pWCET
  • Partition Independence
  • Partition Dominance
  • Full Definition

Library probsa.rt.model.carry_in

Library probsa.rt.model.events

• Fixed Arrival Sequence
• Fixed Job Costs
• Partitions
  • Partition on Arrival Sequences
  • Partition on Job Costs

Library probsa.rt.model.min_inter_arrival

• Minimum Inter-Arrival Time

Library probsa.rt.model.pRBF

Library probsa.rt.model.rt_monotonic

• pRT-Monotonicity
  • Ground Truth System
  • Transformed System
  • Probabilistic Response-Time Monotonicity

Library probsa.rt.model.scheduler

• Scheduler
• Scheduler to Schedule
• RT-Monotonic Scheduler

Library probsa.rt.model.task

• PMF of pWCET
• CDF of pWCET

Library probsa.rt.model.workload

Library probsa.util.bigop

Library probsa.util.bigop_inf

Library probsa.util.boolp

Library probsa.util.etime

Library probsa.util.indicator

Library probsa.util.iota

Library probsa.util.min

Library probsa.util.misc

Library probsa.util.notation

Library probsa.util.prosa.arrival_bound

• Sporadic Arrival Bound

Library probsa.util.prosa.prio_aware

• Ideal Uniprocessor Scheduler Properties

Library probsa.util.prosa.sporadic_as_curve

Library probsa.util.r_mult

Library probsa.util.seq

Library probsa.util.stdpp

• Equality
  • Setoid equality
  • Common properties
• Operations on sets

Library probsa.util.tr_eq

Library probsa.util.zip