PROSA - Formally Proven Schedulability Analysis merge requestshttps://gitlab.mpi-sws.org/mmaida/rt-proofs/-/merge_requests2020-11-02T09:11:04Zhttps://gitlab.mpi-sws.org/mmaida/rt-proofs/-/merge_requests/6delta-min theory2020-11-02T09:11:04ZMarco Maidadelta-min theory1. Theory of **super-additivity**
1. Definition and properties of super-additive functions
2. Minimal extension of a super-additive function
2. Definition and properties of **delta-min *functions***
3. Conversion from **delta-min ...1. Theory of **super-additivity**
1. Definition and properties of super-additive functions
2. Minimal extension of a super-additive function
2. Definition and properties of **delta-min *functions***
3. Conversion from **delta-min to arrival curve**
1. Conversion procedure
2. Proving that the conversion leads to a valid arrival curve
3. Proving that, if a task respects the delta-min, also respects the derived arrival curve
4. Giving a way to reliably bound the search horizon of the conversion procedure on concrete task sets
4. Theory of **delta-min *vectors***
1. Definition and properties
2. Extension of the vector
3. Deriving a delta-min function
Let's discuss about this!https://gitlab.mpi-sws.org/mmaida/rt-proofs/-/merge_requests/4Work-conserving proof2020-02-14T16:16:23ZMarco MaidaWork-conserving proofhttps://gitlab.mpi-sws.org/mmaida/rt-proofs/-/merge_requests/5Adding comments to Prosa2020-02-05T13:23:31ZMarco MaidaAdding comments to Prosahttps://gitlab.mpi-sws.org/mmaida/rt-proofs/-/merge_requests/3Work conserving correctness2020-01-28T20:01:36ZMarco MaidaWork conserving correctnesshttps://gitlab.mpi-sws.org/mmaida/rt-proofs/-/merge_requests/2WIP: Work conservation in EDF, part 22020-01-28T19:21:30ZMarco MaidaWIP: Work conservation in EDF, part 2https://gitlab.mpi-sws.org/mmaida/rt-proofs/-/merge_requests/1Added work conservative schedule definition for EDF2019-11-17T11:30:06ZMarco MaidaAdded work conservative schedule definition for EDFWork-conserving definition for the EDF optimality proofWork-conserving definition for the EDF optimality proof