Règles de Transformation pour la Production Automatique de Systèmes TR2E Critiques

Simplification et structure des transformations

Pour faciliter la compréhension et l’implantation de nos règles de transformation, nous nous appuyons sur les éléments suivants : 1. Nous avons défini une bibliothèque d’interrogateurs des éléments du modèle AADL qui permet l’extraction des informations (structurelles, comportementales, etc.) à partir des composants, des propriétés ou des descriptions comportementales. Ils sont à la fois utilisés dans les préconditions et dans le corps de nos règles de transformation. 2. Pour des raisons de maintenance et d’évolution, nous avons choisi de respecter la syntaxe abstraite du langage Ada définissant les nœuds d’un arbre syntaxique abstrait (AST). Les règles de transformation et les constructions Ada (respectant le profil Ravenscar) produites sont ainsi nommées conformément à la dénomination de la BNF du langage présentée dans l’annexe C de ce manuscrit. 3. Notre processus de raffinement a pris en charge différentes vérifications sur la spécification des composants, notamment la présence des propriétés essentielles pour la définition d’un type ou d’une instance de données, la vérification de la cohérence de la taille mémoire spécifiée vis-à-vis du type, etc. 4. La dernière phase de notre processus de raffinement a éliminé les éléments de modélisation non concrets (extension, prototypes…). Ainsi, la spécification d’un composant contient toutes les propriétés qui lui sont associées (par exemple, il n’y a plus d’héritage). 5. Une routine spécifique (Map_Ada_Name) permet de résoudre les problèmes issus des différentes conventions de nommage entre le langage AADL et le langage Ada (identifiant, nommage des paquetages, etc.). Cette routine est appelée pour l’analyse et la modification (le cas échéant) de tout identifiant AADL rencontré. 

Transformation des composants de données

Cette section présente les règles de transformation assurant la traduction des composants de données AADL vers les types de données, les constantes et les variables globales du langage de programmation Ada. Pour illustrer concrètement la simplicité de nos transformations, nous avons choisi de présenter les règles de transformation vers le langage Ada. Cependant, les patrons de modélisation pour la génération que nous présentons sont généralistes. 148 c 2012 Gilles LASNIER 8.2. Transformation des composants de données Ils peuvent ainsi être réutilisés pour l’expression de règles de transformation vers un autre langage de programmation impératif comme le langage C. L’annexe de modélisation des données du langage AADL (présentée 4) définit les patrons de modélisation des types de données classiques. Ceux-ci reposent sur un ensemble de propriétés AADL spécifiques (l’ensemble de propriétés Data_Model). Nous avons complété ces patrons lors de notre processus de raffinement par les propriétés : Source_Data_Size (propriété issue du standard) exprimant la taille mémoire maximale de la donnée ; Access_Right (propriété issue du standard) exprimant si la donnée est accessible en lecture, en écriture ou en lecture/écriture ; Initial_Value (propriété issue de l’annexe) spécifiant une valeur par défaut pour la donnée modélisée. Ces informations sont utilisées respectivement pour allouer la quantité de mémoire requise (allocation statique…), pour déterminer les types de données, les constantes et les variables, pour l’initialisation du système ou en cas de pannes (liées au caractère asynchrone des communications utilisées par l’intergiciel). Logiquement, ces propriétés permettent de différencier les composants de données AADL et de déterminer la construction Ada équivalente (types de données ou instances, entier signé ou booléen, etc.). Les interrogateurs produits pour chacune de ces propriétés sont, par conséquent, utilisés comme préconditions par nos règles de transformation. Nous distinguons deux catégories de transformation : la transformation des types de données et la transformation des instances de données (constantes et variables). Identification d’une transformation d’un type de donnée Dans le cas des types de données le patron source (le patron d’identification d’un composant) d’une règle de transformation est basé sur une déclaration d’un composant interface ou implantation data spécifiant la propriété Data_Model::Data_Representation (que nous détaillons plus bas). Dans le cas d’un composant de donnée partagée et/ou avec accesseurs, les accesseurs définis dans la déclaration de l’interface du composant et la propriété spécifiant le protocole sélectionné pour la gestion de la concurrence (Concurrency_Control_Protocol) sont ajoutés aux préconditions du patron source. Identification d’une transformation d’une instance de donnée Dans le cas des instances de données, le patron d’identification de la transformation est le suivant : – un composant interface ou implantation data ; – la propriété Data_Model::Base_Type spécifiant le type de l’instance ; – la propriété Access_Right spécifiant si l’instance est accessible en lecture ou en écriture. Cette dernière nous permet de déterminer s’il s’agit d’une variable ou d’une constante. Enfin, la propriété Data_Model::Initial_Value définit une valeur pour l’initialisation de l’instance. Informations structurelles Un composant de donnée AADL est caractérisé par son identifiant, sa catégorie, ses propriétés spécifiques (dans le cas d’un data, l’ensemble de propriétés Data_Model) et, dans le  cas d’un composant implantation, sa structure interne – i.e. ses sous-composants. Ces informations sont utilisées pour générer la construction Ada conformément à la spécification AADL. Nous utilisons la propriété Source_Data_Size pour déterminer précisément le type de donnée Ada équivalent (entier sur 32 bits, entier sur 64 bits, etc.). D’autres propriétés de l’annexe de modélisation des données permettent de déterminer la précision (nombres à virgule flottante), la signature de la donnée, etc. Dans les sections suivantes, nous explicitons nos règles de transformation des composants data AADL vers les types de données du langage Ada.