AADL est dédié à la conception de haut niveau et l'évaluation de systèmes embarqués. Il permet de décrire la structure d'un système et ses aspects fonctionnels par une approche à base de composants. Des processus localement synchrones sont alloués sur une architecture distribuée et communiquent de manière globalement asynchrone (système GALS). Une spécificité du modèle polychrone est qu'il permet de spécifier un système dont les composants peuvent avoir leur propre horloge d'activation : il est bien adapté à une méthodologie de conception GALS. Dans ce cadre, l'atelier Polychrony fournit des modèles et des méthodes pour la modélisation, la transformation et la validation de systèmes embarqués. Cette thèse propose une méthodologie pour la modélisation et la validation de systèmes embarqués spécifiés en AADL via le langage synchrone multi-horloge Signal. Cette méthodologie comprend la modélisation de niveau système en AADL, des transformations automatiques du modèle AADL vers le modèle polychrone, la distribution de code, la vérification formelle et la simulation du modèle polychrone. Notre transformation prend en compte l'architecture du système, décrite dans un cadre IMA, et les aspects fonctionnels, les composants logiciels pouvant être mis en œuvre en Signal. Les composants AADL sont modélisés dans le modèle polychrone en utilisant une bibliothèque de services ARINC. L'annexe comportementale d'AADL est interprétée dans ce modèle via SSA. La génération de code distribué est obtenue avec Polychrony. La vérification formelle et la simulation sont effectuées sur deux études de cas qui illustrent notre méthodologie pour la conception fiable des applications AADL.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00675438 |
| Date | 29 November 2010 |
| Creators | Ma, Yue |
| Publisher | Université Rennes 1 |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | English |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.0013 seconds