Mise en oeuvre de notations standardisées, formelles et semi-formelles dans un processus de développement de systèmes embarqués temps-réel répartis.

In classical Model-Driven Engineering (MDE), one models its system using semi-formal notations, validates and then implements it. The validation step, based upon those models, is critical for distributed, real-time and embedded (DRE) systems. However, this kind of approach is not complete since it does not state how to use those models to perform analysis. There is a need to use a Verification and Validation Driven Engineering approach (V2DE) : models are used to verify the system is built right and to validate it is the right system. This thesis proposes a development process aiming at verification and validation, based upon formal notations. This approach is dedicated to DRE systems. We use a standard architecture description language, AADL, as a pivot language to apply our approach : it allows the engineer to specify his DRE system, from hardware to software concerns. The system relies on a dedicated runtime with specific properties. Our approach takes into account both system's behavioral aspects, and runtime's architectural aspects. We validate the absence of deadlocks, the resources dimensioning, and the schedulability of the system. We also verify that the runtime architecture and services fit together with requirements and effective configuration. Our approach allows to get feedback analysis of both the system and the underlying runtime, in order to refine their model in an iterative development process. In our approach, we transform AADL specifications to the standardized formalism Petri Nets (for the system's behavior validation), and we exploit formal specification in the Z standard notation to verify the AADL runtime, PolyORB.Dans une démarche classique 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, basée sur ces modèles, est particulièrement cruciale pour les systèmes temps-réel répartis et embarqués (TR2E), afin de s'assurer de leur respect d'invariants de sécurité, ou 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. Quels modèles (ou vues) utiliser ? Pour analyser quel type de propriétés ? Ainsi, il est nécessaire d'adopter une démarche d'Ingénierie dirigée par les Vérifications et les Validations (IDV2) : les modèles créés sont ceux qui sont utiles 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 temps-réel réparties embarquées. Nous nous appuyons sur une notation pivot standard pour appliquer cette démarche IDV2 : le langage AADL (Architecture Analysis and Design Language) permet à l'ingénieur de spécifier son application TR2E depuis son architecture matérielle jusqu'à son déploiement logiciel. Il repose sur l'existence d'un exécutif ayant certaines propriétés et proposant différents services. Ce processus prend en compte les aspects comportementaux de l'application ainsi que les aspects architecturaux de l'exécutif. Il repose sur des notations standardisées, permettant de faire face aux problèmes d'interopérabilités des outils mis en oeuvre. Pour l'applicatif, des propriétés comme l'absence d'interblocage, l'utilisation et le dimensionnement de ressources ou encore l'ordonnancement du système sont validées. Pour l'exécutif, le fait que l'architecture de celui-ci et les services proposés sont en adéquation avec les propriétés évoquées lors de sa configuration est vérifié. 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 exploitons et 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