Skip to content
Projects
Groups
Snippets
Help
Loading...
Help
Support
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
R
rt-proofs
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
0
Issues
0
List
Boards
Labels
Milestones
Merge Requests
0
Merge Requests
0
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Analytics
Analytics
CI / CD
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
Maxime Lesourd
rt-proofs
Commits
37d0476e
Commit
37d0476e
authored
Aug 20, 2019
by
jonathan julou
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
encore plus de readme
parent
5a6db6de
Pipeline
#19188
passed with stages
in 3 minutes and 33 seconds
Changes
1
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
30 additions
and
5 deletions
+30
-5
restructuring/README_jonathan.md
restructuring/README_jonathan.md
+30
-5
No files found.
restructuring/README_jonathan.md
View file @
37d0476e
...
...
@@ -131,14 +131,39 @@ and further development suggestions</h1>
<h3>
/restructuring/analysis/analysis_up_to_t/schedulability_up_to_t.v
</h3>
It defines what it means to be a upper or lower response time bound until t,
and then shows the equivalence between being a bound up ot t for all t and
being a general time bound.
and then shows the equivalence between being a bound up ot t for all t and being a general time bound.
<h3>
/restructuring/analysis/analysis_up_to_t/cpa_temporal_step.v
</h3>
It defines what it means to be a upper or lower response time bound until t,
and then shows the equivalence between being a bound up ot t for all t and
being a general time bound.
It uses the abstract model defined in simple_abstracted.v.
The redundant definition of task_input_model and task_model_correct_until_t
should allow tasks to follow different types of arrival models.
Its purpose is the "final result", which states that if all conditions are met,
the WCRTs given by CPA will indeed be upper bounds on the response time for each task.
This uses 2 hypothesis meant to provide analysis on a propagationnal property of the schedule, and an analysis on WCRT.
They have yet to be proved in the exemple of the periodic_jitter_model.
<h3>
/restructuring/analysis/analysis_up_to_t/periodic_jitter_propagation_up_to_t.v
</h3>
There are two sections here.
In the first one, there is a proof of the propagatability of the finite
periodic jitter model, very similar to the one in periodic_jitter_same_law.
However the third hypothesis of that model is thrown away since we use the
2 hypothesis finite model.
In the second one, the above result is used to prove that if all task follow a
periodic with jitter arrival model, and the system verify some reasonnable hypothesis,
then the result of CPA will be correct.
The analysis giving the correction of WCRTs is not done yet.
<h3>
/restructuring/analysis/analysis_up_to_t/up_to_t_definitions.v
</h3>
some definitions of properties that were defined indefinitely that now
have an equivalent up to t.
<h2>
III) Suggestions
</h2>
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment