Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
P
PROSA - Formally Proven Schedulability Analysis
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Build
Pipelines
Jobs
Pipeline schedules
Artifacts
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Terms and privacy
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
RT-PROOFS
PROSA - Formally Proven Schedulability Analysis
Commits
8ca362b2
Commit
8ca362b2
authored
3 years ago
by
Pierre Roux
Browse files
Options
Downloads
Patches
Plain Diff
Clean table of content
parent
056320f0
No related branches found
Branches containing commit
No related tags found
1 merge request
!191
Draft: Initiate a Prosa Tutorial
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
doc/tutorial.v
+5
-111
5 additions, 111 deletions
doc/tutorial.v
with
5 additions
and
111 deletions
doc/tutorial.v
+
5
−
111
View file @
8ca362b2
...
@@ -604,6 +604,8 @@ Model
...
@@ -604,6 +604,8 @@ Model
=====
=====
TODO describe model
TODO describe model
test maths :math:`\sum_{i=1}^n i^2`
|*)
|*)
(*|
(*|
...
@@ -665,121 +667,13 @@ if Coq can compile the `Qed` it managed to check the proof and the new lemma
...
@@ -665,121 +667,13 @@ if Coq can compile the `Qed` it managed to check the proof and the new lemma
is now available for use in future proofs.
is now available for use in future proofs.
|*)
|*)
(*|
Job Properties
--------------
TODO: retrieve/update material from Borislav's document on fixed priority policy and EDF
|*)
(*|
Platform
--------
TODO: retrieve/update material from Borislav's document about schedulers
|*)
(*|
Groups of Jobs
--------------
TODO: retrieve/update material from Borislav's document
|*)
(*|
Job Schedulability
------------------
TODO: retrieve/update material from Borislav's document
|*)
(*|
Busy Interval
-------------
TODO: retrieve/update material from Borislav's document
|*)
(*|
Workload Abstraction and Workload Bounds
----------------------------------------
TODO: retrieve/update material from Borislav's document
|*)
(*|
Tasks with respect to schedules, priorities, workload, service and schedulers
-----------------------------------------------------------------------------
TODO: retrieve/update material from Borislav's document
|*)
(*|
Response Time Bounds
--------------------
TODO: retrieve/update material from Borislav's document
(and maybe move here the definition that was already given much earlier)
|*)
(*|
Tasks Schedulability
--------------------
TODO: retrieve/update material from Borislav's document
|*)
(*|
Task Arrival Bounds
-------------------
TODO: retrieve/update material from Borislav's document
|*)
(*|
Workload bounds
---------------
TODO: retrieve/update material from Borislav's document
|*)
(*|
Task Response-Time Bound
------------------------
TODO: retrieve/update material from Borislav's document
|*)
(*|
Task Response-Time Bound Computation
------------------------------------
TODO: retrieve/update material from Borislav's document
test maths :math:`\sum_{i=1}^n i^2`
|*)
(*|
Task Response-Time Bound Computation
------------------------------------
TODO: retrieve/update material from Borislav's document
should we say a few words about CERTA ?
|*)
(*|
Prosa Parts not Covered in this Document
----------------------------------------
TODO: retrieve/update material from Borislav's document
|*)
(*|
(*|
Contributing
Contributing
============
============
TODO (link to the end of the README)
TODO short conclusion, you should now be able to read doc by yourself
TODO Prosa open source, contributions welcome (link to the end of the README)
|*)
|*)
(*|
(*|
...
...
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment