Dans le paragraphe précédent, nous avons présenté l'ensemble des
spécifications de l'application. Nous avons vu que le langage
MAESTRO est transformé en programme
ESTéREL qui se compile
sous forme d'un automate.
On peut alors envisager de faire des vérifications sur cet
automate, et de valider un certain nombre de propriétés logiques.
Ce travail se fait avec les outils de vérification automatique
dédiés à l'analyse d'automate finis : AUTO/GRAPH [5].
Ces outils permettent d'extraire de l'automate global un automate réduit plus facilement vérifiable pour valider des comportements particuliers. Avec l'interface graphique de l'outil AUTOGRAPH, on peut visualiser les automates résultants.
On peut donc grâce à ces outils détecter des comportements
anormaux, ou vérifier qu'une propriété particulière
est bien réalisée.
La figure 6,
illustre une partie de l'automate, élaboré à travers le langage
de programmation de mission et visualisé grâce à l'outil AUTOGRAPH.
Cette portion de l'automate correspond à la partie de
contrôle de la requête de détection et de suivi de mouvement.
Remarque sur la lecture de l'automate :
Figure 6: Fragment d'automate généré par ESTEREL
Supposons que l'on souhaite vérifier que l'automate suit la politique de transition entre deux TRS, schématisée par la figure 7, et qui concerne la requête de détection et suivi de mouvement.
Figure 7: Déroulement d'une transition entre deux TRS
On va analyser les transitions de l'automate et on vérifie que l'on retrouve bien l'enchaînement des signaux InitOK_ARGES, ReadyToStop_ARGES, Activate, EndKillArges spécifiés pour la transition entre deux TRS dans cet automate.