Processus de Raffinement Incrémental dédié aux Systèmes Critiques

Validation du modèle AADL utilisateur

La figure 7.1 illustre la première étape de notre processus de raffinement. Celle-ci consiste à valider le modèle de l’utilisateur qui sera utilisé comme point d’entrée par notre processus. Celui-ci doit fournir une description complète de l’assemblage des composants architecturaux, des connexions et des informations pour le déploiement des composants logiciels sur la plateforme matérielle cible.  FIGURE 7.1 – Schéma de la phase de validation du modèle AADL utilisateur Pour garantir le déroulement correct de notre processus de raffinement, nous devons nous assurer de : 1. La légalité au sens AADL du modèle initial (syntaxe et sémantique). 

Validation du modèle AADL utilisateur

La compatibilité des composants avec notre profil AADL-HI Ravenscar. 3. La présence des informations de déploiement qui seront utilisées pour la sélection et la configuration des composants intergiciels. 4. L’ordonnançabilité du système avant le raffinement (faisabilité). La vérification de ces éléments garantit la présence de toutes les informations requises comme préconditions pour nos règles de tranformation dédiées au raffinement des composants architecturaux et à la génération des composants intergiciels.

Analyses syntaxique et sémantique

Lors de ces analyses, nous vérifions que le modèle AADL est conforme aux spécifications du standard AADLv2. Il s’agit de la vérification des règles syntaxiques et sémantiques du standard. Les règles sémantiques assurent que la spécification architecturale de l’application est un système réalisable dont l’assemblage des composants est cohérent. Il s’agit notamment, dans notre cas, de nous assurer que : 1. Chaque modèle doit contenir au moins un composant système (composant system) décrivant la hiérarchie des composants spécifiés (pour l’instanciation AADL, voir 4). 2. Dans le cadre d’une application répartie multi-processeurs, chaque système doit contenir au moins un bus de communication reliant les processeurs. 3. Chaque processus doit contenir au moins un fil d’exécution (composant thread). Ces règles peuvent être vérifiées automatiquement à l’aide d’un compilateur dédié au langage AADL (par exemple, OCARINA) ou à l’aide d’un langage de spécification de contraintes (REAL ou OCL).

Analyses supplémentaires

Les analyses supplémentaires concernent la vérification de la spécification correcte des composants de données, des informations de déploiement et du respect des restrictions Ravenscar. Ces analyses sont effectuées en plus de celles réalisées par un outil d’édition de modèles AADL. Le tableau 7.1 récapitule l’ensemble des propriétés AADL impliquées et leur rôle. Types de données Cette vérification vise à satisfaire les contraintes liées aux systèmes critiques sur les données définies dans le chapitre 3. Il s’agit de s’assurer de la spécification de la taille mémoire, de la politique d’accès (lecture et/ou écriture), de la taille bornée des tableaux pour les composants de données. Dans le cas où l’une de ces propriétés est manquante, nous l’indiquons à l’utilisateur, qui peut choisir de modifier ou non son modèle. Si aucune modification n’est apportée, alors nous procédons à l’ajout des propriétés manquantes avec une valeur par défaut lors du raffinement. Restrictions architecturales Ravenscar Nous nous assurons que les restrictions architecturales du profil Ravenscar (RA1, RA2 et RA3, chapitre 3 section 3.4.2) sont satisfaites. Si une restriction est invalidée à cause d’une propriété manquante sur un composant, nous avertissons l’utilisateur qu’une propriété avec une valeur par défaut est ajoutée. Analyse des informations de déploiement Dans le chapitre précédent, nous avons expliqué l’utilité de la spécification des informations de déploiement sur la description architecturale intiale pour la configuration des services intergiciels (tables de routage des nœuds, sélection de la couche basse de transport, etc). Il s’agit essentiellement des propriétés AADL de l’ensemble de propriétés Deployment définies à cet effet. Ainsi, nous nous assurons que : – chaque processus dispose des informations sur sa localisation (IP, PID…) et sur ses ressources matérielles de communication (numéro de port, etc.) ; – chaque processeur spécifie la propriété identifiant la plate-forme sur laquelle le processus (ou nœud) s’exécute ; – chaque bus spécifie les propriétés relatives à la sélection de la couche basse de transport et du protocole. Ces propriétés sont rappelées dans le tableau 7.1. Dans le cas où l’une de ces propriétés est manquante, celle-ci sera générée avec une valeur conventionnelle lors du processus de raffinement.