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
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Build
Pipelines
Jobs
Pipeline schedules
Artifacts
Deploy
Releases
Package Registry
Model registry
Operate
Environments
Terraform modules
Monitor
Incidents
Service Desk
Analyze
Value stream analytics
Contributor analytics
CI/CD analytics
Repository analytics
Model experiments
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
Lasse Blaauwbroek
PROSA - Formally Proven Schedulability Analysis
Graph
77d5fb76422643e6d2370fe0a287de9d7ec21430
Select Git revision
Branches
7
classic-prosa
embed_arr_seq_uniq
fset
master
default
protected
prepare_MC_PR
tutorial
wip-hunspell
Tags
5
v0.5
v0.4
v0.3
v0.2
v0.1
12 results
You can move around the graph by using the arrow keys.
Begin with the selected commit
Created with Raphaël 2.2.0
31
Oct
29
24
23
16
15
11
24
Sep
23
17
30
Aug
23
21
20
13
24
Jul
19
2
27
Jun
26
25
13
12
5
26
May
19
16
13
12
7
3
29
Apr
9
5
12
Oct
19
Sep
4
17
Jul
5
Jan
14
Dec
7
10
Jan
25
Nov
26
Oct
19
18
6
6
Sep
5
Aug
3
17
Jul
15
14
13
12
8
Jun
6
5
May
4
31
Mar
2
23
Feb
16
14
12
7
3
1
20
Jan
19
15
14
13
12
10
9
8
7
6
5
29
Dec
18
17
16
15
14
10
9
8
7
4
3
2
1
30
Nov
24
23
20
18
17
13
10
4
3
28
Oct
27
22
20
16
15
14
13
12
6
1
30
Sep
29
25
22
17
16
15
11
10
9
8
7
6
4
3
1
28
Aug
26
25
24
18
17
12
11
6
5
4
3
31
Jul
30
29
28
27
25
24
22
21
17
16
15
14
13
12
11
10
9
8
7
6
11
Jun
15
May
8
7
6
5
4
30
Apr
22
21
20
23
Mar
6
5
8
Aug
1
31
Jul
30
29
Make cores explicit in ProcessorState
make a few cosmetic tweaks in the EDF optimality proof
make the proof term in the readiness type class "unreferencable"
add CI job for testing against latest ssreflect
make processor state explicit in platform properties
convert comments in behavior module
fix links to Coq standard library in coqdoc output
convert comments in analysis module
update create_makefile.sh to patch up coqdoc.css
convert comments in model
Change definition of service_implies_scheduled
split out service.v + ready.v from schedule.v and add all.v
introduce 'work' as unit of service received or needed
move non-essential job parameter definitions out of behavior
Restructuring the model folder
Update CI configuration for Coq 8.10
Add pretty documentation generation
Shorten a few long proofs
Add seq aRTA
Add lemmas about workload bound
Restructure task arrivals
Add service of set of jobs
Add workload of set of jobs
Polishing base files
Add new util file
Add non-seq aRTA
Add preemption model
Add new generic parameters
Add lemmas about ex_minn
move basic facts out of behavior/ folder
move processor models and properties into model/ directory
update task and job models in preparation of aRTA port
fix definition change fallout in swap analysis
fix definition change fallout in EDF transformation analysis
relate ideal progress model with job completion
fix fallout from definition change in facts/completion.v
note equivalence of assumptions in case of basic readiness
prove ready jobs are incomplete
make definition of completed_jobs_dont_execute uniform
prove jobs must arrive to be ready
Loading