Constructions SysML prises en compte en simulation et pas en vérification
Bonjour,
Les probabilités sur les transitions de machines à états sont prises en compte par la simulateur, pas par le model checker.
Le non prise en compte du temps dans la recherche d'invariants est un autre exemple de construction de langage non supportée par le model checker.
Est-il possible de communiquer sur le site TTool au sujet de ce restriction?
Cordialement
Pierre de Saqui-Sannes, ISAE-SUPAERO, Toulouse
Submitted by external user pdss@isae-supaero.fr