Le modele ROOM formalisation de sa sémantique statique et son application au developpement d'un logiciel de poursuite de satellites

Abstract

Le domaine des systèmes contrôle-commande en temps réel requiert beaucoup de travail au niveau de la spécification du comportement. La demande croissante de ce type de logiciel et les délais de production de plus en plus courts forcent l'utilisation d'outils de développement. Ces derniers doivent permettre d'accélérer le processus de développement et d'en améliorer la qualité.Le modèle ROOM offre un cadre de travail pour la conception et la vérification de systèmes temps-réel. L'outil ObjecTime implante cette technique de modélisation. Il permet de spécifier graphiquement un système, de le simuler et d'en générer le code pour une plate-forme cible. Ce formalisme graphique est accompagné d'un langage textuel (ROOM). Cependant, à cause de la nature du domaine des systèmes contrôle-commande en temps réel, une vérification formelle de la sémantique statique est nécessaire. Elle permet d'accroître la fiabilité de l'outil en éliminant les erreurs dues au langage dans les modèles générés. Sous un autre aspect, l'arrivée récente de cette méthodologie sur le marché implique un manque de maturité. Il lui est donc important d'acquérir de l'expérience sur des problèmes réels. Les résultats de ce mémoire sont un logiciel de poursuite de satellites développé, selon ROOM et une spécification formelle de la sémantique statique du langage ROOM. Une étude de cas a été faite pour vérifier l'application du modèle ROOM à un exemple concret.Le problème choisi n'est pas qu'un simple exemple académique, car le logiciel résultant a été installé dans une station de poursuite de satellites pour vérifier sa qualité. La formalisation du langage est faite à l'aide des grammaires attribuées. Les grammaires attribuées permettent de définir formellement les propriétés des langages contextuels ou non contextuels.Le mémoire présente également une étude préliminaire des outils d'aide à l'implantation d'un compilateur pour le langage et fournit des recommandations quant à ceux-ci.