Modélisation des systèmes temps-réel répartis embarqués pour ...

Sujets

• Modélisation des données
• Éléments du groupe 6
• Message-Oriented Middleware
• Application linéaire
• Données techniques de la tour Eiffel
• Architecture informatique

Informations

• Publié par: Shaum
• Nombre de lectures: 283
• Langue: Français
• Poids de l'ouvrage: 1 Mo

Extrait

École doctorale d’informatique, télécommunications et électronique de Paris Modélisation des systèmes temps-réel répartis embarqués pour la génération automatique d’applications formellement vérifiées erThèse de doctorat soutenue le 1 décembre 2006 par Thomas VERGNAUD pour obtenir le grade de docteur de l’École nationale supérieure des télécommunications – spécialité informatique & réseaux – Composition du jury : rapporteurs : Yvon KERMARREC, professeur à l’École nationale supérieure des télécommunications de Bretagne Jean-François PRADAT-PEYRE, maître de conférence au Conservatoire national des arts et métiers, habilité à diriger des recherches examinateurs : Marie-Pierre GERVAIS, professeur à l’université Paris 10 – Nanterre Frank SINGHOFF, maître de conférence à l’université de Bretagne occidentale directeurs de thèse : Laurent PAUTET, professeur à l’École nationale supérieure des télécommunications de Paris Fabrice KORDON, à l’université Paris 6 – Pierre & Marie Curieccopyright 2007 Thomas VergnaudTelle est la nature de l’esprit humain, telles sont les limites de sa science propre, qu’il n’y a jamais lieu à faire des découvertes toutes nouvelles, mais seulement à éclaircir, vérifier, distinguer dans leur propre source certains faits de sens intime, faits simples, liés à notre existence, aussi anciens qu’elle, aussi évidents, mais qui s’y trouvent enveloppés avec diverses impressions hétéro- gènes qui les rendent vagues et obscurs. Maine DE BIRAN, in Essai sur les fondements de la psychologieRésumé – Modélisation des systèmes temps-réel répartis embarqués pour la génération automatique d’applications formellement vérifiées La construction d’une application répartie fait en général intervenir une couche logicielle par- ticulière, appelée intergiciel, qui prend en charge la transmission des données entre les différents nœuds de l’application. L’usage d’un intergiciel pouvant être adapté aux conditions particulières d’une application donnée s’avère être un bon compromis entre performances et coût de dévelop- pement. La conception d’applications pour les systèmes embarqués temps-réel implique la prise en compte de certaines contraintes spécifiques à ce domaine, que ce soit en terme de fiabilité ou de dimensions à la fois temporelles et spatiales. Ces contraintes doivent notamment être respectées par l’intergiciel. L’objet de ces travaux est la description des applications temps-réel réparties embarquées en vue de configurer automatiquement l’intergiciel adéquat. L’étude se focalise sur la définition d’un processus de conception permettant d’intégrer les phases de description, de vérification et de gé- nération de l’application complète. Pour cela, nous nous reposons sur le langage de description d’architecture AADL. Nous l’ex- ploitons comme passerelle entre la phase de description de l’architecture applicative, les forma- lismes de vérification, la génération du code exécutable et la configuration de l’exécutif réparti. Nous montrons comment spécifier un exécutif pour AADL afin de produire automatiquement le code applicatif et l’intergiciel pour une application répartie. Nous montrons également comment exploiter ces spécifications pour produire un réseau de Petri afin d’étudier l’intégrité des flux d’exécution dans l’architecture. Afin de valider notre processus de conception, nous avons conçu et développé Ocarina, un compilateur pour AADL qui utilise l’intergiciel schizophrène PolyORB comme exécutif. Abstract – Modelling Distributed Real-Time Embedded Systems for the Automatic Generation of Formally Verified Applications Building distributed applications usually relies on a particular software layer, called middle- ware, that manages data transmission between application nodes. Using a middleware that can be adapted to the particular requirements of a given provides a good trade-off between execution performance and development cost. Applications for embedded real-time systems must take specific parameters into account, such as reliability concerns or temporal and spatial constraints. As part of the application, the middle- ware has to respect these constraints also. This work focuses on the description of distributed embedded real-time applications in order to automatically configure the associated middleware. We define a design process that integrates different steps for the description, verification and generation of the complete application. We use the Architecture Analysis & Design Language (AADL) as a backbone between the application description, the verification formalisms, the code generation and the runtime configu- ration. We show how to specify an AADL runtime to automatically generate the application code and the middleware for a given distributed application. We also show how to generate Petri nets from AADL descriptions an how it helps in the verification of the integrity of the execution flows in architectures.To validate this design process, we implemented Ocarina, an AADL compiler that uses Poly- ORB, a schizophrenic, highly tailorable middleware, as a runtime.Table des matières Avant-propos xi I Introduction 1 I-1 Adaptabilité des intergiciels . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 I-2 Vers une démarche systématique pour la construction d’intergiciels adaptés . . . 2 I-3 Organisation de la thèse . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 II Description de la configuration d’une application répartie 7 II-1 Adaptation des intergiciels . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 II-1.1 Relation entre l’intergiciel et l’application . . . . . . . . . . . . . . . . 7 II-1.2 Description des caractéristiques de l’application . . . . . . . . . . . . 7 II-2 Approches centrées sur l’intergiciel . . . . . . . . . . . . . . . . . . . . . . . . 8 II-2.1 Bibliothèque de communication . . . . . . . . . . . . . . . . . . . . . 8 II-2.2 Adaptation de l’intergiciel aux interfaces de l’application . . . . . . . . 8 II-2.3 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 II-3 Approches centrées sur l’application . . . . . . . . . . . . . . . . . . . . . . . 14 II-3.1 Déclinaisons orientées composant des spécifications « classiques » . . . 14 II-3.2 Conception de l’application par agencement de composants . . . . . . 16 II-3.3 Isolation des informations de déploiement . . . . . . . . . . . . . . . . 16 II-3.4 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 II-4 Conception des applications fondée sur les modèles . . . . . . . . . . . . . . . 17 II-4.1 Présentation d’UML . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 II-4.2 Particularisation de la syntaxe UML . . . . . . . . . . . . . . . . . . . 19 II-4.3 La démarche MDA . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 II-4.4 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 II-5 Vers une description formelle des applications . . . . . . . . . . . . . . . . . . 20 II-5.1 Aperçu des langages de description d’architecture . . . . . . . . . . . 20 II-5.2 Éléments constitutifs de la d’une architecture . . . . . . . . 21 II-5.3 Langages pour assister la production de systèmes exécutables . . . . . 22 II-5.4 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 II-6 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 II-6.1 Insuffisances des approches centrées sur l’intergiciel . . . . . . . . . . 26 II-6.2 Spécifications concrètes de l’application . . . . . . . . . . . . . . . . . 27 II-6.3 AADL comme langage pour la configuration d’intergiciel . . . . . . . 27 c 2007 Thomas Vergnaud viiModélisation des systèmes temps-réel répartis embarqués III AADL, un langage pour décrire les architectures 29 III-1 Principes du langage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 III-2 Définition des composants . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 III-2.1 Catégories de composants . . . . . . . . . . . . . . . . . . . . . . . . 30 III-2.2 Types et implantations . . . . . . . . . . . . . . . . . . . . . . . . . . 31 III-3 Structure interne des composants . . . . . . . . . . . . . . . . . . . . . . . . . 32 III-3.1 Sous-composants . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 III-3.2 Appels de sous-programmes . . . . . . . . . . . . . . . . . . . . . . . 33 III-4 Les éléments d’interface . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 III-4.1 Les ports . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 III-4.2 Les sous-programmes d’interface . . . . . . . . . . . . . . . . . . . . 35 III-4.3 Les accès à sous-composant . . . . . . . . . . . . . . . . . . . . . . . 35 III-4.4 Synthèse sur les éléments d’interface . . . . . . . . . . . . . . . . . . 35 III-5 Connexions des composants . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 III-5.1 Les connexions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 III-5.2 Les flux . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 III-5.3 Matérialisation des connecteurs . . . . . . . . . . . . . . . . . . . . . 39 III-6 Configurations d’architecture . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 III-6.1 Développement et instanciation des déclarations . . . . . . . . . . . . 39 III-6.2 Les modes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 III-7 Espaces de noms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 III-8 Propriétés et annexes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 III-8.1 Propriétés . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 III-8.2 Annexes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 III-8.3 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 III-9 Évolutions de la syntaxe d’AADL . . . . . . . . . . . . . . . . . . . . . . . . . 46 III-9.1 Modélisation des séqu