dvojtise
commented
7 years ago This use case may raise interesting research issues and dev features such as:
- [dev/research] generalize the possibility to have user event in the sequential engine (ie. the scenario) this would increase the priority for this gemoc feature that we've already discussed in the past
- [research] synthesis of traces are used for generating attack trees but this abstraction/grouping of traces can also be useful in order to analyze model execution traces (for test purpose for example)
Currently, ATSyRA uses a conversion to GAL (https://lip6.github.io/ITSTools-web/gal.html) in order to get its behavior implementation and use ITS model checker for efficient search.
However ITS model checker has limitation, it doesn't provide the state of the variables, only the transition. This is good for verification of the trees, but this is limiting while trying to synthetize attack trees.
As Atsyra studio is already partly based on gemoc commons component (+ sirius and xtext) providing an alternative implementation using the gemoc sequential engine would be interresting in order to fill the gap left by the mode checker.
Additionnaly the trace viewers would provide a convenient tool box for merging traces identified by the model checker and help to build the attack tree.
The animation will probably also be a nice-to-have feature.