Abstract FR:

Dans un processus d'ingénierie dirigée par les modèles (IDM), l'ingénieur modélise son système à l'aide d'une notation semi-formelle, le valide puis l'implante. L'étape de validation est cruciale pour les systèmes temps-réel répartis et embarqués (TR2E), pour s'assurer de leur bon fonctionnement logique ou temporel. Cependant, une démarche IDM n'est pas suffisante car elle n'indique pas comment utiliser les modèles pour faire des analyses. Il est nécessaire d'adopter une démarche d'Ingénierie Dirigée par les Vérifications et les Validations (IDV2) pour s'assurer que le système est correctement construit(vérification), et qu'il satisfait un ensemble de propriétés spécifiées en amont dans le processus de développement (validation). Cette thèse propose un processus de développement, de validation et de vérification basé sur des notations formelles, et dédié aux applications TR2E. Le langage AADL(Architecture Analysis and Design Language) est utilisé comme notation pivot. Le processus proposé prend en compte les aspects comportementaux de l'application et les aspects architecturaux de l'exécutif. Il repose sur des notations standardisées, pour faire face aux problèmes d'interopérabilités des outils mis en oeuvre. Notre démarche permet d'obtenir des retours aussi bien à propos de l'applicatif que de l'exécutif, et permet de corriger ou modifier les modèles dans un processus de développement itératif. Au cours de notre démarche, nous transformons les spécifications AADL vers différentes notations standardisées : les réseaux de Petri pour la validation de l'applicatif, la notation Z pour la vérification de l'exécutif utilisé, PolyORB.