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

É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équences d’appel . . . . . . . . . . . . . . . . . . . 47 III-9.2 Connexion des paramètres . . . . . . . . . . . . . . . . . . . . . . . . 49 III-10 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 IV Utilisation d’AADL pour décrire une application répartie 53 IV-1 Utilisation d’AADL pour décrire le déploiement d’une application . . . . . . . 53 IV-1.1 Identification des composants pour la description de la topologie . . . . 53 IV-1.2 Intégration des informations de déploiement . . . . . . . . . . . . . . 55 IV-1.3 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 IV-2 Vers un développement conjoint de l’application et de l’intergiciel . . . . . . . 58 IV-3 Cycle de dév . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59 IV-3.1 Principes du prototypage . . . . . . . . . . . . . . . . . . . . . . . . . 59 IV-3.2 Phases de conception . . . . . . . . . . . . . . . . . . . . . . . . . . . 59 IV-4 Utilisation d’AADL pour le cycle de développement . . . . . . . . . . . . . . . 61 IV-4.1 Conception d’un exécutif pour AADL . . . . . . . . . . . . . . . . . . 61 IV-4.2 Structuration de la description . . . . . . . . . . . . . . . . . . 62 IV-4.3 Matérialisation de la modélisation de l’intergiciel . . . . . . . . . . . . 64 IV-5 Spécifications de l’exécutif AADL . . . . . . . . . . . . . . . . . . . . . . . . 64 IV-5.1 Relation avec les descriptions comportementales . . . . . . . . . . . . 65 IV-5.2 Interprétation des séquences d’appel . . . . . . . . . . . . . . . . . . . 65 IV-5.3 Description des modèles de répartition . . . . . . . . . . . . . . . . . . 66 cviii 2007 Thomas VergnaudTable des matières IV-5.4 Cycle de fonctionnement des threads . . . . . . . . . . . . . . . . . . 69 IV-6 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70 V Génération du code pour l’enveloppe applicative 71 V-1 Identification des éléments applicatifs d’AADL . . . . . . . . . . . . . . . . . 71 V-2 Traduction des composants AADL applicatifs en langage de programmation . . 72 V-2.1 Organisation du processus de traduction . . . . . . . . . . . . . . . . . 72 V-2.2 Traduction des composants de données . . . . . . . . . . . . . . . . . 73 V-2.3 T des sous-programmes . . . . . . . . . . . . . . . . . . . . 76 V-2.4 Gestion des entités distantes . . . . . . . . . . . . . . . . . . . . . . . 85 V-2.5 Organisation des fichiers générées . . . . . . . . . . . . . . . . . . . . 86 V-3 Traduction des composants applicatifs en langage Ada . . . . . . . . . . . . . . 86 V-3.1 Traduction des espaces de nom . . . . . . . . . . . . . . . . . . . . . 87 V-3.2 T des composants de donnée . . . . . . . . . . . . . . . . . . 87 V-3.3 Traduction des sous-programmes . . . . . . . . . . . . . . . . . . . . 88 V-4 Traduction des composants AADL applicatifs dans d’autres langages . . . . . . 90 V-4.1 Traduction vers C . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 90 V-4.2 T vers Java . . . . . . . . . . . . . . . . . . . . . . . . . . . 91 V-5 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97 VI Construction et configuration de l’interface avec l’intergiciel d’exécution 99 VI-1 Spécifications de l’intergiciel d’exécution . . . . . . . . . . . . . . . . . . . . . 99 VI-1.1 Sémantique des threads AADL . . . . . . . . . . . . . . . . . . . . . 100 VI-1.2 Niveau des services fournis par l’intergiciel d’exécution . . . . . . . . 101 VI-2 Première phase : utilisation d’un intergiciel de haut niveau . . . . . . . . . . . . 101 VI-2.1 Organisation de l’interface avec l’intergiciel . . . . . . . . . . . . . . . 102 VI-2.2 Application à l’intergiciel PolyORB . . . . . . . . . . . . . . . . . . . 103 VI-3 Seconde phase : utilisation d’un intergiciel de bas niveau . . . . . . . . . . . . 107 VI-3.1 Expansion des threads AADL . . . . . . . . . . . . . . . . . . . . . . 107 VI-3.2 Transposition de l’architecture schizophrène en AADL . . . . . . . . . 108 VI-3.3 Modélisation en AADL de l’interface avec l’intergiciel . . . . . . . . . 109 VI-3.4 du cœur de l’intergiciel en AADL . . . . . . . . . . . . . 110 VI-3.5 Assemblage des composants . . . . . . . . . . . . . . . . . . . . . . . 116 VI-3.6 Évaluation des caractéristiques des services de communications . . . . 118 VI-4 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 118 VII Vérification formelle de la structure des applications 121 VII-1 Objectifs de la vérification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 121 VII-1.1 Éléments de vérification . . . . . . . . . . . . . . . . . . . . . . . . . 121 VII-1.2 Définition des réseaux de Petri . . . . . . . . . . . . . . . . . . . . . . 122 VII-2 Principes de la traduction des constructions AADL en réseaux de Petri . . . . . 124 VII-3 Définition des domaines de couleur du réseau . . . . . . . . . . . . . . . . . . 125 VII-4 Modélisation des éléments de haut niveau . . . . . . . . . . . . . . . . . . . . 125 VII-4.1 Traduction des composants . . . . . . . . . . . . . . . . . . . . . . . . 125 VII-4.2 T des connexions . . . . . . . . . . . . . . . . . . . . . . . . 128 VII-5 Modélisation de l’implantation des composants . . . . . . . . . . . . . . . . . . 133 VII-5.1 Modélisation des sous-composants . . . . . . . . . . . . . . . . . . . . 133 c 2007 Thomas Vergnaud ixModélisation des systèmes temps-réel répartis embarqués VII-5.2 Modélisation des sous-programmes . . . . . . . . . . . . . . . . . . . 133 VII-5.3 des séquences d’appel de sous-programmes . . . . . . . 135 VII-5.4 Exemple complet . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 137 VII-6 Intégration des descriptions comportementales . . . . . . . . . . . . . . . . . . 140 VII-6.1 Composant sans modélisation comportementale . . . . . . . . . . . . . 140 VII-6.2 Composant possédant une description comportementale . . . . . . . . 140 VII-6.3 Séquence d’appel pure . . . . . . . . . . . . . . . . . . . . . . . . . . 141 VII-6.4 Composant hybride . . . . . . . . . . . . . . . . . . . . . . . . . . . . 141 VII-7 Propriétés étudiées sur l’architecture . . . . . . . . . . . . . . . . . . . . . . . 142 VII-7.1 Cohérence des communications . . . . . . . . . . . . . . . . . . . . . 142 VII-7.2 Absence de blocages . . . . . . . . . . . . . . . . . . . . . . . . . . . 145 VII-7.3 Déterminisme des valeurs . . . . . . . . . . . . . . . . . . . . . . . . 146 VII-8 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 147 VIII Mise en pratique 149 VIII-1 Ocarina, un compilateur pour AADL . . . . . . . . . . . . . . . . . . . . . . . 149 VIII-1.1 Principes généraux . . . . . . . . . . . . . . . . . . . . . . . . . . . . 149 VIII-1.2 Structure du modèle d’Ocarina . . . . . . . . . . . . . . . . . . . . . . 151 VIII-1.3 Organisation d’Ocarina . . . . . . . . . . . . . . . . . . . . . . . . . . 152 VIII-1.4 Intégration dans des applications tierces . . . . . . . . . . . 155 VIII-2 Évaluation des performances d’exécution . . . . . . . . . . . . . . . . . . . . . 156 VIII-2.1 Définition de l’architecture AADL . . . . . . . . . . . . . . . . . . . . 156 VIII-2.2 Mise en place des applications-témoins . . . . . . . . . . . . . . . . . 160 VIII-2.3 Résultats . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 164 VIII-3 Évaluation de la transformation en réseaux de Petri . . . . . . . . . . . . . . . . 165 VIII-3.1 Motifs AADL de base . . . . . . . . . . . . . . . . . . . . . . . . . . 166 VIII-3.2 Exemple de taille réelle . . . . . . . . . . . . . . . . . . . . . . . . . 167 VIII-3.3 Étude de l’application de test . . . . . . . . . . . . . . . . . . . . . . . 168 VIII-4 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 169 IX Conclusions et perspectives 171 IX-1 Conception conjointe de l’application et l’intergiciel . . . . . . . . . . . . . . . 171 IX-1.1 AADL comme support pour un cycle de conception . . . . . . . . . . 172 IX-1.2 Exploitation des descriptions AADL . . . . . . . . . . . . . . . . . . . 172 IX-2 Perspectives . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 173 IX-2.1 Production automatique d’intergiciels en AADL . . . . . . . . . . . . 173 IX-2.2 Raffinement des spécifications de l’exécutif . . . . . . . . . . . . . . . 174 IX-2.3 Automatisation de la réduction des architectures . . . . . . . . . . . . 174 IX-2.4 Correspondances entre AADL et d’autres représentations . . . . . . . . 174 IX-2.5 Reconfiguration dynamique de l’exécutif . . . . . . . . . . . . . . . . 174 IX-2.6 Intégration dans la démarche MDA . . . . . . . . . . . . . . . . . . . 175 cx 2007 Thomas Vergnaud