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.

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

revise and extend SysML specification #30

Open
3 of 18 tasks
kiniry opened this issue Nov 9, 2021 · 6 comments
Open
3 of 18 tasks

revise and extend SysML specification #30

kiniry opened this issue Nov 9, 2021 · 6 comments
Assignees
Labels
ACSL Matters related to ACSL specifications and/or the use of Frama-C. architecture assurance Issues that relate to the assurance of the system, whether via models, code, informal, or formal. cryptol Issues related to our Cryptol specifications, or use thereof. documentation Issues that relate to documentation about the system, including user and developer docs, source code ENHANCEMENT New feature or request feature model FEATURE Lando/Lobot Issues related to our Lando or Lobot specifications. Someday Issues that are not required by our current contract, but we'd like to attend to someday. specifications Issues that relate to system specifications, whether of models, code, protocols, or otherwise. SysML Issues related to our SysML specifications, or use thereof. verification
Milestone

Comments

@kiniry
Copy link
Member

kiniry commented Nov 9, 2021

  • bump our SysML v2 Pilot Implementation version to the January 2022 release
  • revise scenarios to reflect final design and V&V (see revise scenario specifications to reflect final system under V&V #45)
  • revise events to reflect final design and V&V (see revise events specifications to reflect final system under V&V #44)
  • write definitions for all Project Glossary concepts that are incomplete
  • further refactor and collect Project Glossary terms into sub-packages
  • alphabetize Project Glossary, per-sub-package, per-package
  • complete Physical Architecture by wiring up parts using cables and channels
  • complete RTS Implementation Artifacts specification by defining dataflow on provided items
  • encode Cryptol state machine into SysML state machine
  • core ASM specification in SysML (depends on revise events specifications to reflect final system under V&V #44 for event specs)
  • specify model normal behavior and exceptional behaviors, lifted from the Cryptol model, using Occurences, Time Slices, and Snapshots, mapping Occurences to Messages on device driver actions
  • ensure that the appropriate invariants of the ACSL model are lifted to SysML Constraint
  • figure out the appropriate means by which to lift and express ACSL models and contracts into the SysML model
  • transliterate FRET requirements into SysML requirements
  • transliterate NRC characteristics into SysML requirements
  • add any necessary traceability properties and annotations that are not implicitly covered by our methodology
  • after Lando/Lobot feature model is complete, lift that model into SysML as a variability model
  • itemize necessary architecture view and generate beautiful renderings of every view for presentations and report
@kiniry kiniry added documentation Issues that relate to documentation about the system, including user and developer docs, source code specifications Issues that relate to system specifications, whether of models, code, protocols, or otherwise. FEATURE architecture On Deck SysML Issues related to our SysML specifications, or use thereof. labels Nov 9, 2021
@kiniry kiniry added this to the Task 1: Implementation milestone Nov 9, 2021
@kiniry
Copy link
Member Author

kiniry commented Nov 9, 2021

This issue is ready to be owned by @abakst and @podhrmic as they lean into learning SysML and evolving the system specification.

@kiniry
Copy link
Member Author

kiniry commented Dec 18, 2021

As covered in #40, many of these subtasks are immaterial to the initial implementation, thus I'm moving this issue to Task 2 and we'll complete these secondary specification tasks during V&V.

@kiniry
Copy link
Member Author

kiniry commented Jan 14, 2022

I have started the transliteration of FRET and Lando requirements into SysML. See the new elements in the Requirements package. To complete the relevant task, the remaining/missing requirements from the FRET model need to be added to the SysML model, and model elements necessary to formally express said requirements in FRET have to be lifted to the SysML model. Doing so permits one to specify the necessary attributes and constraint expressions. See 5dbaf30.

@kiniry
Copy link
Member Author

kiniry commented Jan 15, 2022

Behaviors that use SysML Occurances &c are refined from our event/action specs once they are complete.

@kiniry
Copy link
Member Author

kiniry commented Jan 20, 2022

Per my message on ~HARDENS, I'm going to take ownership of this issue to drive all revisions of the SysML model to completion. I'm going to open a top-level branch on this.

@kiniry kiniry added ACSL Matters related to ACSL specifications and/or the use of Frama-C. assurance Issues that relate to the assurance of the system, whether via models, code, informal, or formal. cryptol Issues related to our Cryptol specifications, or use thereof. ENHANCEMENT New feature or request feature model Lando/Lobot Issues related to our Lando or Lobot specifications. verification and removed On Deck labels Feb 18, 2022
@kiniry
Copy link
Member Author

kiniry commented Oct 27, 2022

All of the above tasks are nice-to-haves at this point, and we can take them on again as we revise the SysMLv2 model in future IR&D or project work. As such, I'm moving this back to a Someday issue with no milestone.

@kiniry kiniry removed this from the Task 2: Validation and Verification milestone Oct 27, 2022
@kiniry kiniry added Someday Issues that are not required by our current contract, but we'd like to attend to someday. and removed WiP labels Oct 27, 2022
@kiniry kiniry added this to the SysML milestone May 22, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
ACSL Matters related to ACSL specifications and/or the use of Frama-C. architecture assurance Issues that relate to the assurance of the system, whether via models, code, informal, or formal. cryptol Issues related to our Cryptol specifications, or use thereof. documentation Issues that relate to documentation about the system, including user and developer docs, source code ENHANCEMENT New feature or request feature model FEATURE Lando/Lobot Issues related to our Lando or Lobot specifications. Someday Issues that are not required by our current contract, but we'd like to attend to someday. specifications Issues that relate to system specifications, whether of models, code, protocols, or otherwise. SysML Issues related to our SysML specifications, or use thereof. verification
Projects
None yet
Development

No branches or pull requests

2 participants