Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Extend model by protocol sessions #47

Closed
senier opened this issue Mar 12, 2019 · 0 comments · Fixed by #382
Closed

Extend model by protocol sessions #47

senier opened this issue Mar 12, 2019 · 0 comments · Fixed by #382
Assignees
@senier
Labels
model Related to model package (e.g., model verification)
Projects
RecordFlux 0.5

Comments

@senier
Copy link
Member

senier commented Mar 12, 2019 •
edited

Extend the RecordFlux model by a concept to express automata, including states, transitions, conditions and actions. Dynamic properties should be expressible by some temporal logic.

As an intermediate step, when no session syntax is available, we use the YAML-based representation introduced for GreenTLS. To develop and validate those models, the cli is extended to parse the YAML sessions files.
@senier senier created this issue from a note in RecordFlux Future (To do) Mar 12, 2019
@senier senier removed this from To do in RecordFlux Future May 8, 2020
@senier senier added this to To do in RecordFlux 0.5 via automation May 8, 2020
@senier senier changed the title Support dynamic protocol semantics Protocol sessions Jun 4, 2020
@senier senier changed the title Protocol sessions Extend model by protocol sessions Jun 17, 2020
@senier senier added the model Related to model package (e.g., model verification) label Jun 17, 2020
This was referenced Jun 17, 2020
Closed
Closed
Closed
@treiher treiher moved this from To do to In progress in RecordFlux 0.5 Jul 24, 2020
senier pushed a commit that referenced this issue Aug 1, 2020
Use existing QuantifiedExpression
ddd905f 
Ref. #47
senier pushed a commit that referenced this issue Aug 1, 2020
Replace (Not)Contains by (Not)In
3505a91 
Ref. #47
senier pushed a commit that referenced this issue Aug 1, 2020
Reintroduce StateName
fbba11e 
At least in our current TLS models, state names may have (multiple) dots, which
is incompatible with ID. It sounds preferable, in general, to have a distinct
name space for states anyways.

Ref. #47
senier pushed a commit that referenced this issue Aug 1, 2020
Check channel parameter only for builtins
8754eca 
Ref. #47
senier pushed a commit that referenced this issue Aug 1, 2020
Fix validate and add TLS session files
66061c1 
Ref. #47
senier pushed a commit that referenced this issue Aug 1, 2020
Replace SubprogramCall by Call
7a3a09f 
Ref. #47
senier pushed a commit that referenced this issue Aug 1, 2020
Prevent code generator from substituting literal field names
b4bda68 
Ref. #47
senier pushed a commit that referenced this issue Aug 1, 2020
Add output directory for session graph
156057a 
Ref. #47
senier pushed a commit that referenced this issue Aug 1, 2020
Improve test coverage
f4d8c6d 
Ref. #47
@senier senier moved this from In progress to Ready in RecordFlux 0.5 Aug 1, 2020
@senier senier mentioned this issue Aug 1, 2020
Merged
This was referenced Aug 11, 2020
Closed
Closed
treiher added a commit that referenced this issue Aug 11, 2020
@treiher
Replace StateName by ID
552e1b0 
Ref. #47, #382
treiher added a commit that referenced this issue Aug 11, 2020
@treiher
Move declarations into separate module
cb2853b 
Ref. #47, #382
treiher added a commit that referenced this issue Aug 11, 2020
@treiher
Use abstractmethod decorator
1941b11 
Ref. #47, #382
treiher added a commit that referenced this issue Aug 11, 2020
@treiher
Make declarations self-contained
cb1f242 
Ref. #47, #382
treiher added a commit that referenced this issue Aug 11, 2020
@treiher
Remove unused enum literal
1c1379a 
Ref. #47, #382
treiher added a commit that referenced this issue Aug 11, 2020
@treiher
Remove FIXME
95c9861 
Ref. #47, #382
senier pushed a commit that referenced this issue Aug 18, 2020
@treiher
Remove unused enum literal
75fdc2d 
Ref. #47, #382
senier pushed a commit that referenced this issue Aug 18, 2020
@treiher
Remove FIXME
3e6883e 
Ref. #47, #382
senier pushed a commit that referenced this issue Aug 18, 2020
@treiher
Change method order
a38c8ab 
Ref. #47, #382
senier pushed a commit that referenced this issue Aug 18, 2020
@treiher
Replace classmethod by staticmethod
87994d3 
Ref. #47, #382
senier pushed a commit that referenced this issue Aug 18, 2020
@treiher
Move simple test yaml-file from specs into tests
d114a11 
Ref. #47, #382
senier pushed a commit that referenced this issue Aug 18, 2020
@treiher
Remove unnecessary immutable flag in tests
1997539 
Ref. #47, #382
senier pushed a commit that referenced this issue Aug 18, 2020
@treiher
Move tests into appropriate test modules
46e4c24 
Ref. #47, #382
RecordFlux 0.5 automation moved this from Ready to Merged Aug 19, 2020
treiher pushed a commit that referenced this issue Aug 19, 2020
@treiher
Use existing QuantifiedExpression
347173c 
Ref. #47
treiher pushed a commit that referenced this issue Aug 19, 2020
@treiher
Replace (Not)Contains by (Not)In
286f1b7 
Ref. #47
treiher pushed a commit that referenced this issue Aug 19, 2020
@treiher
Reintroduce StateName
bd90b5d 
At least in our current TLS models, state names may have (multiple) dots, which
is incompatible with ID. It sounds preferable, in general, to have a distinct
name space for states anyways.

Ref. #47
treiher pushed a commit that referenced this issue Aug 19, 2020
@treiher
Check channel parameter only for builtins
e114159 
Ref. #47
treiher pushed a commit that referenced this issue Aug 19, 2020
@treiher
Fix validate and add TLS session files
3d9fba9 
Ref. #47
treiher pushed a commit that referenced this issue Aug 19, 2020
@treiher
Replace SubprogramCall by Call
78f3c07 
Ref. #47
treiher pushed a commit that referenced this issue Aug 19, 2020
@treiher
Prevent code generator from substituting literal field names
9d28fe1 
Ref. #47
treiher pushed a commit that referenced this issue Aug 19, 2020
@treiher
Add output directory for session graph
6a95e4c 
Ref. #47
treiher pushed a commit that referenced this issue Aug 19, 2020
@treiher
Improve test coverage
126a333 
Ref. #47
treiher added a commit that referenced this issue Aug 19, 2020
@treiher
Replace StateName by ID
176a6e9 
Ref. #47, #382
treiher added a commit that referenced this issue Aug 19, 2020
@treiher
Move declarations into separate module
67e5cb5 
Ref. #47, #382
treiher added a commit that referenced this issue Aug 19, 2020
@treiher
Use abstractmethod decorator
c2f7673 
Ref. #47, #382
treiher added a commit that referenced this issue Aug 19, 2020
@treiher
Make declarations self-contained
1cb0e16 
Ref. #47, #382
treiher added a commit that referenced this issue Aug 19, 2020
@treiher
Remove unused enum literal
634a081 
Ref. #47, #382
treiher added a commit that referenced this issue Aug 19, 2020
@treiher
Remove FIXME
9e955e2 
Ref. #47, #382
treiher added a commit that referenced this issue Aug 19, 2020
@treiher
Change method order
45d0662 
Ref. #47, #382
treiher added a commit that referenced this issue Aug 19, 2020
@treiher
Replace classmethod by staticmethod
ae0a0b4 
Ref. #47, #382
treiher added a commit that referenced this issue Aug 19, 2020
@treiher
Move simple test yaml-file from specs into tests
d568207 
Ref. #47, #382
treiher added a commit that referenced this issue Aug 19, 2020
@treiher
Remove unnecessary immutable flag in tests
debc8e9 
Ref. #47, #382
treiher added a commit that referenced this issue Aug 19, 2020
@treiher
Move tests into appropriate test modules
13dbcff 
Ref. #47, #382
@treiher treiher mentioned this issue Aug 4, 2021
Closed
9 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@senier senier

Labels
model Related to model package (e.g., model verification)
Projects
No open projects
RecordFlux 0.5
  
Merged
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Issue 47: Extend model by protocol sessions AdaCore/RecordFlux
1 participant
@senier