Merge requests · RT-PROOFS / PROSA - Formally Proven Schedulability Analysis

Prove that abstract search space is a subset of RS-FP search space

!352 · created Jan 22, 2024 by Sergey Bozhko
- Merged
- 16
updated Jan 23, 2024
Refactor assumptions in a lemma about RBF

!354 · created Jan 23, 2024 by Sergey Bozhko
- Merged
- 1
updated Jan 23, 2024
De-duplicate [blocking_bound]

!350 · created Jan 19, 2024 by Sergey Bozhko
- Merged
- 9
updated Jan 22, 2024
Prove lemmas about restricted supply proc. and change SBF def

!349 · created Jan 19, 2024 by Sergey Bozhko
- Merged
- 3
updated Jan 19, 2024
Add I/IW instantiation for restricted supply

!348 · created Jan 18, 2024 by Sergey Bozhko
- Merged
- 17
updated Jan 19, 2024
Prove existence of abstract busy interval

!347 · created Jan 16, 2024 by Sergey Bozhko
- Merged
- 25
- 1
updated Jan 18, 2024
generalize proof and improve structure

!346 · created Jan 15, 2024 by Sergey Bozhko
- Merged
- 5
updated Jan 16, 2024
restructure I/IW instantiation files

!345 · created Jan 15, 2024 by Sergey Bozhko
- Merged
- 26
updated Jan 15, 2024
release jitter propagation

!341 · created Jan 08, 2024 by Björn Brandenburg
- Merged
- 7
updated Jan 15, 2024
Define some notions about workload and service + clean up

!344 · created Jan 12, 2024 by Sergey Bozhko
- Merged
- 12
updated Jan 15, 2024
Service inversion is bounded

!343 · created Jan 10, 2024 by Sergey Bozhko
- Merged
- 9
updated Jan 12, 2024
improve terminology about priority inversion

!342 · created Jan 10, 2024 by Sergey Bozhko
- Merged
- 1
updated Jan 10, 2024
Introduce notion of service inversion

!339 · created Jan 04, 2024 by Sergey Bozhko
- Merged
- 75
updated Jan 10, 2024
Improve SBF-definition structure

!340 · created Jan 05, 2024 by Sergey Bozhko
- Merged
- 9
updated Jan 06, 2024
Add sequential restricted-supply aRTA

!319 · created Jul 05, 2023 by Sergey Bozhko
- Merged
- 98
updated Jan 04, 2024
CI: use locally hosted Docker images

!338 · created Jan 03, 2024 by Björn Brandenburg
updated Jan 03, 2024
remove Makefile patching and fix links in spec

!337 · created Jan 03, 2024 by Björn Brandenburg
updated Jan 03, 2024
define restricted supply processor model

!261 · created Feb 24, 2023 by Sergey Bozhko
- Merged
- 42
updated Dec 12, 2023
enforce strict subproofs

!334 · created Nov 17, 2023 by Kimaya Bedarkar
- Merged
- 38
updated Nov 24, 2023
fix "nonuniform inheritance" deprecation warning

!336 · created Nov 23, 2023 by Björn Brandenburg
updated Nov 23, 2023