Modélisation des systèmes temps-réel répartis embarqués pour ...
203
pages
Français
Documents
Le téléchargement nécessite un accès à la bibliothèque YouScribe Tout savoir sur nos offres
203
pages
Français
Ebook
Le téléchargement nécessite un accès à la bibliothèque YouScribe Tout savoir sur nos offres
É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 ...
Voir
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 ...
É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
© 2010-2024 YouScribe
