Le logiciel EADS ST, qui fonctionne en mode automatique, doit prendre en compte les perturbations externes, de même que les différentes défaillances du matériel susceptibles de se produire pendant le vol. L'étude de cas examine dès lors les points les plus pertinents pour l'application intégrée du logiciel et se concentre sur le comportement critique en temps réel.

Le logiciel EADS ST combine des comportements asynchrones et des comportements synchrones cycliques au sein du même processus. Les comportements asynchrones incluent notamment l'allumage et la séparation des étages, l'isolation des défaillances et la récupération, tandis que les comportements synchrones cycliques englobent le contrôle/la commande de la navette et la détection des pannes.

Certaines questions particulières ont été soulevées. L'une d'elles concerne les difficultés associées à la combinaison du comportement cyclique et acyclique, qui conduit à une explosion de l'espace d'état. À cause de ce problème, les chercheurs ont en effet dû utiliser des techniques d'abstraction. Une autre question importante mise en évidence par l'étude de cas est la validation de la politique de programmation utilisée par le logiciel du lanceur, qui repose sur un programme préemptif à priorité fixe.

Le modèle UML, qui a été conçu dans le cadre de l'outil Rational Rose, a utilisé des outils IFx/IF tels qu'un vérificateur de sémantique, un simulateur et un vérificateur de modèles, de sorte qu'il peut être validé. Outre leur comportement en temps réel, ces outils ont le grand avantage d'être compatibles avec la sémantique OMEGA.

Le simulateur, en particulier, permet de corriger de nombreuses erreurs, telles que les interblocages imprévus présents au sein du modèle et non décelés par un examen manuel. Les outils et la méthodologie utilisés dans cette étude de cas feront prochainement l'objet d'un article.