Skip to content

GitLab

Explore

Sign in

Primary navigation

Project

P

PROSA - Formally Proven Schedulability Analysis
- Activity
- Members
- Labels

Snippets Groups Projects

d8354ce5

Commit d8354ce5 authored 1 year ago by Sergey Bozhko

Downloads
- Patches
- Plain Diff

generalize proof of busy interval from no-carry-in

parent 5cc06028

No related branches found

No related tags found

1 merge request!363Prove RTA for RS-FP-EDF and RS-NP-EDF

Changes 3

Hide whitespace changes

Inline Side-by-side

Showing

analysis/abstract/ideal/iw_instantiation.v 5 additions, 1 deletion

analysis/abstract/ideal/iw_instantiation.v
analysis/facts/busy_interval/carry_in.v 53 additions, 40 deletions

analysis/facts/busy_interval/carry_in.v
analysis/facts/model/ideal/service_of_jobs.v 83 additions, 14 deletions

analysis/facts/model/ideal/service_of_jobs.v

with 141 additions and 55 deletions

Loading

0% Loading or .

You are about to add 0 people to the discussion. Proceed with caution.

Finish editing this message first!

Please register or sign in to comment