search

GaloisInc / HARDENS

Repository for the HARDENS project
Apache License 2.0
18 stars 1 forks source link

revise scenario specifications to reflect final system under V&V #45

Closed kiniry closed 2 years ago

kiniry commented 2 years ago

During Task 2 we must revise our scenario specifications (in Lando and SysML) to reflect those events that exist in the Cryptol model and the demonstrator implementation. Like our final SysML<->Cryptol model revisions at the end of Task 1, this often means small changes on both ends of the refinement relation, but usually amounts to just some renaming to make the refinement plain.

kiniry commented 2 years ago

Note that scenarios and events are specified using Actions in SysMLv2.

kiniry commented 2 years ago

I have sketched out the necessary revisions of the RTS system (testable) scenarios in test_scenarios.lando and in the SysML model in commit 8b37cee. What is missing from my sketch is (a) the trivial normal scenario of the system operating under normal environmental conditions. Based upon this sketch I believe that @abakst should be able to finish the spec.

kiniry commented 2 years ago

All test scenarios are documented in the Lando specification and are realized in the model-based parametrized tests found in the tests folder. In particular, see the tests/scenarios folder.