Library probsa.rt.behavior.schedule

• Probabilistic Schedule

Library probsa.rt.behavior.response_time

• Probabilistic Response Time

Library probsa.rt.behavior.service

• Probabilistic Service

Library probsa.rt.behavior.arrival_sequence

• Probabilistic Arrival Sequence
• Additional Definitions
  • job_arrival → pr_arrival_sequence for Job : Finite
• Lemmas

Library probsa.rt.behavior.job

• Probabilistic Parameters of a Job
• Derived Notions

Library probsa.rt.model.min_inter_arrival

• Minimum Inter-Arrival Time

Library probsa.rt.model.WCET

• Worst-Case Execution Time

Library probsa.rt.model.rt_monotonic

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

Library probsa.rt.model.task

• PMF of pWCET
• CDF of pWCET

Library probsa.rt.model.events

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

Library probsa.rt.model.scheduler

• Scheduler
• Scheduler to Schedule
• RT-Monotonic Scheduler

Library probsa.rt.model.axiomatic_pWCET

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

Library probsa.rt.analysis.partition_transfer

• Partition Transfer

Library probsa.rt.analysis.axiomatic_pWCET_full

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

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.completion

• Probabilistic Completion is Monotone

Library probsa.rt.analysis.WCET_is_pWCET

• WCET is Axiomatic pWCET

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.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.probability.law_of_total_prob

• Law of Total Probability

Library probsa.probability.partition

Library probsa.probability.cdf

Library probsa.probability.conditional

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

Library probsa.probability.nrvar

• Natural Random Variable
• Notation Instances

Library probsa.probability.prob

• Additional 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.brvar

• Boolean Random Variable
• Notation Instances

Library probsa.probability.stochastic_order

Library probsa.probability.pred

Library probsa.util.etime

Library probsa.util.iota

Library probsa.util.stdpp

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

Library probsa.util.indicator

Library probsa.util.notation

Library probsa.util.bigop_inf

Library probsa.util.bigop

Library probsa.util.misc

Library probsa.util.boolp