Abstract FR:

Cette thèse propose une approche qui permet de coupler l'utilisation de méthodes formelles avec celle de techniques de développement objet ou fonctionnel. Dans cette approche, la conception, basée sur l'utilisation d'outils tels que Uim / x, fournit une description de l'Interface dans les langages Uil et C. De cette description est extrait un modèle formel Lustre qui sert à la vérification de propriétés à satisfaire par l'Interface. La description de celle-ci peut alors être améliorée en fonction des propriétés analysées sur le modèle. La modélisation ainsi que la vérification des propriétés génériques sont automatisées alors que l'expression et la vérification des propriétés spécifiques s'appuient sur un éditeur graphique. L'automatisation et l'éditeur graphique évitent au concepteur d'avoir à connaître le formalisme Lustre. Cette approche permet donc l'utilisation transparente d'un formalisme tout en préservant des techniques plus classiques de développement telles que les techniques objets ou fonctionnelles. Ce processus de développement tente ainsi d'améliorer la conception des Interfaces.