Une fois les différentes TRS spécifiées et les vues abstraites associées établies, il faut pouvoir élaborer des missions complexes à partir de ces différentes actions.
Cet arrangement de TRS se fait au niveau contrôle à travers le formalisme des Procédures Robot ou PRS et l'utilisation du langage MAESTRO. Les PRS représentent la spécification d'un arrangement de plusieurs TRS dans le but de réaliser un objectif global. Cette gestion des TRS est assuré par la spécification des PRS sous forme d'un comportement logique.
La traduction du comportement logique des PRS se fait en langage ESTEREL, et de manière automatique grâce au langage de programmation de mission : MAESTRO [4].
Ce langage utilise directement les vues abstraites des différentes actions et permet grâce à une syntaxe définie dans [4] de les arranger afin d'élaborer une mission, dans notre cas notre application.
Une fois la mission programmée, en utilisant la syntaxe de MAESTRO,
un automate est généré qui va contrôler le comportement de
l'application.
Cet automate pourra être ensuite utilisé pour établir des vérifications
du comportement de l'application et pour prouver que certaines
propriétés des spécifications sont bien vérifiées.
La figure 5 illustre l'interface graphique utilisée par le langage de programmation de mission pour définir le comportement des PRS, i.e. les différents enchaînements d'actions à gérer.
Figure 5: Interface de programmation de MAESTRO