Niveau d’Abstraction Pour l’Analyse et la Génération de Code

Composants requis pour l’analyse Rappel

La vérification d’un système vise à s’assurer que celui-ci est correctement construit et sa validation vise à garantir le respect de ses spécifications. Validation et vérification s’effectuent au travers de différentes analyses reposant sur une abstraction structurée et complète modélisant un aspect particulier du système. Ces aspects sont liés à la satisfaction de contraintes relatives à la spécificité du système. Le langage AADL permet d’exprimer des contraintes fonctionnelles et non fonctionnelles sous une forme condensée et structurée au sein d’une représentation unique. Il sert de point d’entrée pour procéder à l’analyse du système ou de langage pivot pour la production d’un modèle d’analyse dans un formalisme tiers. Dans cette section, nous rappelons les différentes contraintes inhérentes aux systèmes TR2E critiques. Puis, nous nous intéressons aux principaux outils d’analyse basés sur AADL et plus particulièrement aux composants AADL et à leurs attributs (propriétés…) qu’ils utilisent. Ces éléments nous permettent de déterminer la granularité du composant AADL et le niveau d’abstraction requis pour différentes analyses.

Composants requis pour l’analyse 

Contraintes spécifiques aux systèmes critiques Afin de déterminer les composants AADL les plus pertinents requis par les outils d’analyse, nous proposons une classification simple des contraintes fonctionnelles et non fonctionnelles à satisfaire dans le contexte des systèmes TR2E critiques. Cette classification nous permet de distinguer les caractéristiques des différentes suites d’outils supportant une modélisation AADL. Ainsi, nous distinguons six familles de contraintes : 1. les contraintes sur la cohérence de la modélisation : conformité de la description architecturale, hiérarchie entre composants, sémantique des composants ; 2. les contraintes structurelles : informations de déploiement, préparation de l’application en vue de la distribuer (critère distribué de l’application) ; 3. les contraintes sur la consommation des ressources matérielles et logicielles : utilisation processeur, bande passante, empreinte mémoire (critère embarqué de l’application) ; 4. les contraintes temporelles : respect d’échéances temporelles, ordonnançabilité (critère temps-réel de l’application) ; 5. les contraintes de criticité : intégrité des données, sûreté de fonctionnement, sécurité, tolérances aux pannes, déterminisme ; 6. les contraintes comportementales : validation du comportement vis-à-vis des spécifications de l’utilisateur, équité, interblocage, vivacité, etc. Dans la sous-section suivante, nous présentons les principaux outils d’analyse visant la vérification d’une ou plusieurs de ces contraintes.

Vérification et validation de modèles AADL

Le tableau 5.1 synthétise les principaux outils et les familles de contraintes qu’ils vérifient. Pour certaines plates-formes d’intégration (par exemple TASTE ou AADL INSPECTOR intégrant l’outil CHEDDAR), nous ne considérons que les fonctionnalités supplémentaires offertes ou intégrées. OSATE2 OCARINA CHEDDAR TASTE TINA AADL INSPECTOR Cohérence x x x x Structurelles x Ressources x x x x Temporelles x x x Criticité x x Comportement x x TABLE 5.1 – Contraintes et outils d’analyses AADL OSATE2 OSATE2 [SEI/CMU, 2011] est une plate-forme dédiée à l’analyse et à l’intégration d’outils basés sur les modèles AADL. La partie frontale permet de vérifier la cohérence de la description (syntaxe et sémantique des composants). Un certain nombre de plugins d’analyse assurent aussi la vérification de propriétés de sécurité et de sûreté, du flot d’exécution des données, de l’allocation et de la consommation mémoire, de l’intégrité et de la cohérence des données, de la consommation d’énergie et de la propagation d’erreurs. c 2012 Gilles LASNIER 83 Chapitre 5. Niveau d’Abstraction Pour l’Analyse et la Génération de Code Tous les composants AADL sont supportés. Les analyses sont effectuées à partir d’un modèle déclaratif AADL ou d’un modèle d’instance généré par OSATE2. Celui-ci décrit une instance du système modélisé où les liens d’extension, de raffinement, de protypage et certains calculs sur les valeurs de propriétés sont résolus. OCARINA OCARINA [TELECOM ParisTech, 2012] propose une partie frontale assurant l’analyse de la cohérence d’une description architecturale et des informations structurelles (déploiement, répartition) pour la génération du système. Différentes analyses à travers l’implantation du langage de contraintes REAL et l’exportation de modèles vers le formalisme des réseaux de Petri ou vers l’outil CHEDDAR sont possibles : – l’annexe AADL-REAL [Gilles, 2008] permet la vérification de contraintes et le calcul d’expressions complexes sur les modèles architecturaux AADL. Elle supporte un sousensemble de composants (matériels et logiciels) et leurs propriétés associées. Il permet la vérifiation de la cohérence du dimensionnement d’une application (projet MOSIC), des spécifications (respect des patrons de modélisation, respect des restrictions du profil AADL/Ravenscar) et des exigences de sécurité et sûreté au sein de la plate-forme POK. – OCARINA/RDP est une partie dorsale permettant la transformation des composants architecturaux AADL vers les réseaux de Petri. Ainsi, nous pouvons vérifier le comportement d’un système par l’analyse de contraintes telles l’absence d’interblocage, la famine, la vivacité ou l’équité dans une application répartie (multi-tâches) contenant des ressources partagées. Le mapping des composants AADL vers les constructions des réseaux de Petri est décrit dans [Renault, 2009] (chapitre 4, section 4.1.1) et nécessite les composants suivants : sous-programmes, threads, processeurs, variable partagée, port. Les propriétés AADL standards pour ces composants sont aussi requises. Enfin, les composants systèmes et processus sont utilisés pour structurer la spécification et apportent des informations hiérarchiques sous la forme d’espace de nommage permettant la traçabilité des résultats de la vérification et la détection de composants fautifs. CHEDDAR CHEDDAR permet la vérification de performances et de l’ordonnançabilité d’un système modélisé en AADL. Dans [Singhoff et al., 2005], les auteurs décrivent quels sont les éléments du langage AADL pris en compte pour l’analyse d’ordonnancement, à savoir : les composants de données (variable partagée), les accesseurs aux composants de données, les threads, les processus, les processeurs et les composants systèmes. CHEDDAR utilise certaines propriétés AADL standards mais aussi un ensemble de propriétés AADL (pour les composants de données, threads, processeurs) spécifiques à l’analyse d’ordonnancement. Enfin, CHEDDAR permet à l’aide de la spécification des ports de threads d’effectuer une analyse mémoire sur la taille et la capacité des tampons pour les communications entre threads. TASTE (MAST) TASTE [Perrotin et al., 2011] est une plate-forme d’intégration assurant l’interopérabilité entre différents outils pour le développement et l’analyse de systèmes TR2E. Ainsi, TASTE intégre de nombreux outils tels OCARINA (pour la génération), CHEDDAR, MAST, MARZHIN (pour l’analyse), etc. Nous nous intéressons, ici, uniquement à l’intégration de l’outil . Composants requis pour l’analyse pour l’analyse de l’ordonnancement du système. MAST nécessite une transformation des éléments architecturaux du langage AADL vers les éléments du méta-modèle MAST. Le mapping de AADL vers MAST est exprimé dans [Perrotin et al., 2011] (chapitre 16, section 5). Ainsi, les composants processeur, thread, sous-programme, bus, périphérique et les composants de données sont utilisés. Un sous-ensemble des propriétés standards AADL associées à ces composants est requis. AADL-FIACRE-TINA L’outil TINA permet l’analyse comportementale de réseaux de Petri et de systèmes temporisés. Dans [Berthomieu et al., 2010], les auteurs proposent une transformation de modèles AADL vers FIACRE pour exprimer le comportement, les aspects temporels et la sémantique d’exécution du système puis une transformation de modèles FIACRE vers le formalisme pris en compte par TINA. Les auteurs décrivent les composants architecturaux et les éléments de l’annexe comportementale AADL transformés. L’annexe comportementale utilisée ici est une ancienne version de celle présentée chapitre 4, basée sur le langage AADL 1.0 et n’intégrant pas de langage d’expression aussi détaillé que la nouvelle. Ainsi, les composants inclus sont les composants threads, les ports de threads, les composants de données (variable partagée), les accesseurs aux composants de données, les modes et les constructions de l’annexe comportementale relatives aux threads. Un sous-ensemble de propriétés AADL standards dédiées à ces composants est aussi employé. AADL INSPECTOR (MARZHIN) AADL INSPECTOR [Ellidiss Technologies, 2012] est un outil d’analyse extensible basé sur l’expression et la vérification de règles sur les modèles AADL. Nous nous intéressons ici à la simulation du système avec MARZHIN. Pour ce faire, l’outil fournit une transformation de modèle AADL vers le formalisme d’entrée de MARZHIN. Le sous-ensemble AADL supporté concerne les composants processeur, thread, les ports d’événements, les données (variable partagée), les accesseurs de données, les appels de sous-programmes et les constructions de l’annexe comportementale pour les threads et les sous-programmes. Un sous-ensemble des propriétés AADL standards spécifiques à ces composants est aussi utilisé pour la transformation.