Meeting SCADE - SpaceEx 20 Oct. 2015
Date: Oct 30, 2015 3:30 am – Oct 30, 2015 7:30 am
Discussion meeting on a possible translation between SCADE & SpaceEx
Participants:
Esterel: X. Fornari, B Pagano, JL Colaco, C. Pasteur
UJF: Goran Frehse
Center of discussion was to understand both technologies and see what could be actually done.
SpaceEx uses a formal specification to automatically generates observers to build proofs. The input format is hybrid automata which also provides non-deterministic description
Going from SCADE to SpaceEx depends on the domain. We also consider SCADE Hybrid, which the extension of SCADE with continuous support (see Pouzet-Pagano-Caillaud)
- Continuous to continuous: ok, quite easy
- Boolean computation (control): could be ok, with unfolding
- Discrete computation: this is the problem, could such computation be considered as constraints ?
We could consider state unfolding, if not too many. In any cases the customer has to provide information required for the verification.
SpaceEx can also access to an external model to provide computation results. In which case, invariants must be provided to SpaceEx
An interesting example illustrating the difference. A lunar module, that tries to land. If h < L, then boost. This takes into account the past state (PID). This cannot be put in SpaceEx, and abstraction is need.
A possible solution would be to use cosimulation techniques to avoid some recomputation.
Decision is take to establish regular contacts to work on the topic.
Submitted by Xavier Fornari
on
Discussion meeting on a possible translation between SCADE & SpaceEx
Participants:
Esterel: X. Fornari, B Pagano, JL Colaco, C. Pasteur
UJF: Goran Frehse
Center of discussion was to understand both technologies and see what could be actually done.
SpaceEx uses a formal specification to automatically generates observers to build proofs. The input format is hybrid automata which also provides non-deterministic description
Going from SCADE to SpaceEx depends on the domain. We also consider SCADE Hybrid, which the extension of SCADE with continuous support (see Pouzet-Pagano-Caillaud)
- Continuous to continuous: ok, quite easy
- Boolean computation (control): could be ok, with unfolding
- Discrete computation: this is the problem, could such computation be considered as constraints ?
We could consider state unfolding, if not too many. In any cases the customer has to provide information required for the verification.
SpaceEx can also access to an external model to provide computation results. In which case, invariants must be provided to SpaceEx
An interesting example illustrating the difference. A lunar module, that tries to land. If h < L, then boost. This takes into account the past state (PID). This cannot be put in SpaceEx, and abstraction is need.
A possible solution would be to use cosimulation techniques to avoid some recomputation.
Decision is take to establish regular contacts to work on the topic.