Brevet FR3056782A1 — publié le 20180330

GÉNÉRATION DE CODES APPLICATIFS À PARTIR D'UNE SPÉCIFICATION FORMELLE DOMAINE DE L'INVENTION La présente invention se rapporte au domaine de génération de codes applicatifs exécutables par un processeur à partir d'une spécification formelle associée à une application et, plus particulièrement, concerne des codes pour des fonctions applicatives de type contrôle, commande, asservissement, logiques opérationnelles, etc. Actuellement, les fonctions applicatives embarquées (en particulier dans les aéronefs) sont typiquement spécifiées sous forme de planches de type SCADE permettant ensuite d'utiliser des langages de type LUSTRE pour générer automatiquement des codes embarqués correspondants. Ce genre de langage est usuellement basé sur un ensemble fini de symboles qui peuvent être simples (par exemple, un ET à deux entrées) ou complexes (par exemple, une détection de changements de signes sur une période donnée). La génération du code exécutable embarqué consiste donc à instancier la suite de symboles qui est identifiée dans la spécification applicative. Traditionnellement, il est choisi un mode de génération qui consiste à prendre chaque symbole chaque fois qu'il doit être exécuté. Par exemple, si 10 symboles ET doivent être exécutés consécutivement, le code produit contiendra 10 fois le code binaire de l'opération ET. Ce principe de génération présente l'avantage d'être simple et assure une bonne maitrise du code qui sera exécuté par le calculateur ce qui est une propriété importante pour ce type de logiciel certifié. En particulier, la traduction directe de la spécification en un code déterminé est testée une fois pour toute, ce qui permet d'alléger fortement la vérification du code final. Toutefois, cette technique usuelle produit un code très volumineux pouvant réduire l'efficacité de l'exécution. En effet, le fait de générer un code très volumineux, sans opportunité de rémanence des plans mémoires de type caches dans un processeur de haute performance, impose une forte utilisation du plan mémoire lent du processeur ce qui réduit l'efficacité de l'exécution de ce type de logiciel fortement linéaire. De plus, l'exécution d'un code fortement linéaire sur un premier coeur du processeur sature la bande passante offerte par le plan mémoire lent. De ce fait, l'exécution d'un autre code 3056782 2 similaire par un deuxième coeur est peu efficace car les deux coeurs se ralentissent mutuellement. On notera également que la forte dépendance au plan mémoire lent peut induire des interférences entre les divers coeurs. En outre, l'enchainement des symboles induit beaucoup de séquences d'accès 5 mémoire. Les accès peuvent ainsi se mélanger, se permuter, ou se repousser compliquant par conséquent, le chronométrage ou la caractérisation de la séquence complète d'accès. En particulier, la performance des processeurs modernes est très sensible à la typologie des accès mémoires et, de ce fait, le défaut de caractérisation de ces accès induit une très grande difficulté pour déterminer avec certitude « le pire cas de temps d'exécution » WCET 10 (Worst Case Execution Time) ce qui peut être très pénalisant dans un contexte d'application de type « contrôle » ou « commande ». Par ailleurs, la technique usuelle de production de code embarqué infère un grand nombre d'accès en cas de traitement de données une à une (de type Fetch). Ainsi, le temps d'exécution d'une application est constitué en majeure partie du temps nécessaire 15 pour charger le code dans le processeur. C'est un effet induit par l'absence de contributeurs majeurs du temps d'exécution dans le code produit. Ainsi, les techniques actuelles de génération de codes embarqués sont antagonistes de l'évolution contemporaine des processeurs. Il en résulte une utilisation fortement sous-optimale de ces processeurs. 20 L'objet de la présente invention est, par conséquent, de remédier aux inconvénients précités en proposant un procédé et un système de génération d'un code embarqué adapté pour tirer profit au maximum de la puissance intrinsèque des nouveaux processeurs. 25 OBJET ET RÉSUMÉ DE L'INVENTION La présente invention vise à générer automatiquement un code applicatif compact adapté pour tirer profit de la puissance intrinsèque des processeurs. L'invention concerne un procédé et un système de génération d'un code applicatif exécutable par un processeur à partir d'une spécification formelle associée à une application, ladite 30 spécification formelle comprenant des opérateurs, ledit système comportant un analyseur 3056782 3 configuré pour coder chaque opérateur de ladite spécification formelle par un code-opération correspondant suivi d'un nombre minimal de code(s)-entrée(s) et code-sortie identifiant des paramètres d'entrées et de sortie associés audit opérateur, générant ainsi automatiquement un code applicatif compact adapté pour être stocké dans une mémoire 5 associée au processeur et pour être exécuté par un interpréteur stocké dans une mémoire du processeur. Ceci permet de transformer de manière efficace la spécification formelle en un code applicatif formel très compact en termes de volume qui peut être chargé dans le processeur en un temps très réduit, tout en étant parfaitement compréhensible par 10 l'interpréteur associé au processeur. Ainsi, en utilisant une représentation compacte du code applicatif formel, la présente invention permet de réduire la charge de travail imposée à la ressource mémoire, ceci dans le but d'obtenir un temps d'exécution amélioré pour des applications d'un certain profil et particulièrement pour des systèmes multi-coeurs où la ressource mémoire est limitée et le nombre de coeurs plutôt en excès. En outre, grâce au 15 fait que les accès sont moins nombreux, et sont contrôlés par l'interpréteur dont le code est fixe, il est plus aisé de prédire la séquence et la chronologie des accès à la mémoire. Le « pire cas de temps d'exécution » des logiciels applicatifs est ainsi déterminé avec une très grande précision. Ainsi, on optimise fortement l'utilisation des processeurs hautes performances intégrant plusieurs coeurs numériques. 20 Avantageusement, l'analyseur est configuré pour définir comme implicite au moins un des paramètres d'entrée et de sortie de chaque symbole appartenant à un sous-ensemble de symboles spécifiques. Ceci permet de compresser encore davantage le code applicatif. Avantageusement, le code applicatif est un code dans lequel chaque code- 25 opération et/ou chacun des code(s)-entrée(s) et code-sortie sont représentés par un champ de bits prédéterminé. Ceci permet de bien formater le code applicatif, d'optimiser sa structure, de réduire sa taille et de faciliter sa production. 3056782 4 A titre d'exemple, le code applicatif peut être un code octal, dans lequel chaque code-opération et/ou chacun des code(s)-entrée(s) et code-sortie sont représentés par un octet ou un multiple d'octets. Egalement, à titre d'exemple, la spécification formelle peut être une 5 représentation graphique formelle. Avantageusement, le système comporte un interpréteur configuré pour être stocké en totalité ou au moins en partie dans la mémoire cache de premier niveau du processeur, ledit interpréteur étant adapté pour décoder et exécuter les instructions du code applicatif au fur et à mesure de leur lecture. Ceci permet de tirer avantage des 10 mémoires-caches en y logeant l'interpréteur dans une mémoire cache de premier niveau du processeur. Avantageusement, l'interpréteur est configuré pour lire chaque code-opération courant, pour déduire le nombre et le type de paramètres, pour trouver des pointeurs associés auxdits paramètres, pour déterminer des spécifications implicites et pour exécuter 15 le code-opération courant. Ainsi, l'interpréteur décode rapidement et efficacement le code applicatif au fil de l'eau comme une simple table de configuration. Avantageusement, l'interpréteur est configuré pour s'alimenter par anticipation de phase des éléments du code applicatif stocké dans une mémoire interne ou 20 externe. Ceci permet de masquer ces temps d'accès avec un gain supplémentaire d'efficacité. L'invention vise également un calculateur avionique comportant un processeur intégrant un interpréteur et un code applicatif généré par le système selon l'une quelconque des caractéristiques précédentes. 25 Ainsi, le calculateur présente une plus forte intégration dans l'aéronef et/ou une plus grande capacité d'accueil de fonctions avioniques plus gourmandes en puissance de calcul, améliorant ainsi davantage les performances de l'aéronef. L'invention vise aussi un aéronef comportant au moins un calculateur avionique selon les caractéristiques ci-dessus. 3056782 5 L'invention vise également un procédé de génération d'un code applicatif exécutable par un processeur à partir d'une spécification formelle associée à une application, ladite spécification formelle comprenant des opérateurs, ledit procédé comportant les étapes suivantes : 5 - générer automatiquement un code applicatif compact en codant chaque opérateur de ladite spécification formelle par un code-opération correspondant suivi d'un nombre minimal de code(s)-entrée(s) et/ou code-sortie identifiant des paramètres d'entrées et de sortie associés audit opérateur, - stocker ledit code applicatif dans une mémoire associée à un processeur, et 10 - exécuter ledit code applicatif par un interpréteur stocké dans une mémoire du processeur. BRÈVE DESCRIPTION DES DESSINS D'autres particularités et avantages du système et du procédé selon l'invention 15 ressortiront mieux à la lecture de la description faite ci-après, à titre indicatif mais non limitatif, en référence aux dessins annexés sur lesquels : - la Fig. 1 illustre de manière schématique un système de génération d'un code applicatif, selon un mode de réalisation de l'invention ; - la Fig. 2 illustre de manière schématique un procédé de génération d'un 20 code applicatif destiné à être embarqué dans un processeur, selon un mode de réalisation de l'invention ; - la Fig. 3 illustre un exemple d'une planche d'une partie de la spécification formelle d'une application, selon l'invention ; et - la Fig. 4 illustre de manière schématique une partie fonctionnelle d'un 25 processeur, selon l'invention. DESCRIPTION DÉTAILLÉE DE MODES DE RÉALISATION Le principe de l'invention consiste à utiliser une technique spécifique de compression de code et de gestion de mémoires caches pour tirer profit de la puissance 30 intrinsèque des processeurs actuels. 3056782 6 La Fig. 1 illustre de manière schématique un système de génération d'un code applicatif, selon un mode de réalisation de l'invention. Le système 1 de génération de code comporte une unité de traitement 3 comprenant un analyseur 5 et des unités de stockage 7. 5 L'analyseur 5 est configuré pour générer un code applicatif 9 formel (i.e. précis et sans aucune ambiguïté) exécutable par un processeur à partir d'une spécification formelle 11 associée à une application. La spécification formelle 11 spécifie l'application par des séquences d'un nombre restreint de fonctions élémentaires comportant des opérateurs (ou symboles) B1-B3 arithmétiques et/ou logiques. A titre d'exemple, la 10 spécification formelle 11 peut être de forme analytique, graphique ou autre. Plus particulièrement, l'analyseur 5 est configuré pour coder automatiquement chaque opérateur (ou symbole) de la spécification formelle 11 par un code-opération correspondant (dit opcode) suivi éventuellement d'un nombre minimal (pouvant être nul) de code(s)-entrée(s) (i.e. codes-opérandes) et de code-sortie identifiant des paramètres ou 15 arguments d'entrées et de sortie associés à l'opérateur. Le codage automatique de tous les opérateurs visés dans la spécification formelle 11 génère un code applicatif 9 compact. Ce dernier est adapté pour être stocké dans une mémoire associée au processeur (ou microprocesseur) et pour être exécuté par un interpréteur stocké dans une mémoire du processeur. De façon particulière, un opérateur (ou symbole) peut ne pas comporter de 20 code-entrée (respectivement de code sortie) tout en étant prévu pour acquérir une valeur d'un capteur, lire un bus numérique... (respectivement commander un actionneur, écrire sur un bus numérique...) correspondant de façon implicite (par définition) à cet opérateur. On notera qu'il y a des informations qu'on peut spécifier de manière implicite. En particulier, pour certains symboles, on peut déduire le nombre de paramètres associés 25 et le type de paramètre (nombre d'entiers, nombre de flottants, etc.). En effet, parmi l'ensemble de tous les symboles, il existe un sous-ensemble comprenant des symboles spécifiques dont au moins une partie des paramètres peuvent être considérés comme implicites car il n'existe aucune ambigüité. Ce sous-ensemble comporte des symboles courts de type NON, EXPOSANT, VALEUR ABSOLUE, etc. ainsi que des symboles logiques. 30 Par exemple, le symbole NON comporte un code-opération (i.e. l'opération de négation), 3056782 7 un code-entrée et un code-sortie. Toutefois, les paramètres d'entrée et de sortie peuvent être considérés (sans aucune ambigüité) comme implicites permettant ainsi de réduire la taille du codage. Par ailleurs, les symboles logiques peuvent aussi être considérés comme comportant des paramètres implicites lorsque la valeur retour de chaque symbole logique 5 est préservée dans un registre dédié du processeur. Ainsi, l'analyseur 5 est avantageusement configuré pour définir comme implicite au moins un des paramètres d'entrées et de sortie de chaque symbole appartenant au sous-ensemble de symboles spécifiques. La présente invention permet ainsi d'optimiser le taux de compression tout en 10 permettant un décodage efficace adapté pour être appliqué au cas spécifique des processeurs multi-coeurs et rapides. Par ailleurs, le code applicatif 9 généré est un code dans lequel chaque code- opération et/ou chacun des code(s)-entré(s) et code-sortie sont représentés avantageusement par un champ de bits (bit-field) prédéterminé sélectionné de manière à 15 optimiser la structure du code applicatif. A titre d'exemple, le code applicatif 9 peut être un code octal (dit bytecode). Ainsi, chaque code-opération et/ou chacun des code(s)entré(s) et code-sortie sont représentés par un octet ou un multiple d'octets (n-octets). On notera que le code applicatif 9 compact généré par l'analyseur 5 ainsi que l'interpréteur 13 associé sont d'abord stockés dans les moyens de stockage 7 du système 1 20 de génération avant qu'ils soient embarqués dans des processeurs. En particulier, l'interpréteur 13 est un automate logiciel (i.e. un programme informatique) très compact qui contient la signification de chacun des symboles de la représentation graphique formelle. Ainsi, lorsque l'interpréteur est chargé dans un processeur, il permet à ce dernier d'exécuter le code applicatif. 25 La Fig. 2 illustre de manière schématique un procédé de génération d'un code applicatif destiné à être embarqué dans un processeur, selon un mode de réalisation de l'invention. L'étape El concerne la production d'un programme informatique d'interprétation qui contient la signification de chacun des opérateurs ou symboles B1-Bn 30 pouvant être utilisé par la spécification formelle. Ce programme d'interprétation 3056782 8 correspond ainsi à l'automate logiciel de l'interpréteur 13 qui va être utilisé pour interpréter le code applicatif 9. On notera que la spécification formelle comporte un nombre assez réduit d'opérateurs B1-Bn, permettant ainsi de construire un interpréteur très compact ce qui 5 permet son exécution dans un plan mémoire ultra rapide du processeur. A titre d'exemple, la spécification formelle peut être définie selon une représentation graphique construite à partir d'un environnement de type SCADE qui comporte un nombre réduit de symboles. Plus particulièrement, lorsque le code applicatif 9 est représenté par un code octal (byte-code) on aura une limite de 256 symboles. Bien entendu, lorsque le code applicatif 9 est 10 représenté par un champ de bits, la seule limite est la taille des mémoires internes du processeur. L'interpréteur 13 va être utilisé en permanence pour lire et exécuter le code applicatif 9 avec une rapidité extrême par rapport à l'art antérieur. En effet, au lieu de générer un code pour chacune des fonctions (comme dans l'art antérieur), la présente 15 invention produit juste quelques mots codés et c'est l'interpréteur 13 stocké dans la ou les mémoire(s) rapide(s) qui contient la signification de chacun des symboles. L'étape E2 concerne la construction par l'analyseur 5 du code applicatif 9 formel à partir de la spécification formelle 11. A titre d'exemple, lorsque la spécification formelle correspond à une représentation graphique, elle peut être composée de plusieurs 20 planches comprenant chacune un circuit de symboles. En effet, la Fig. 3 illustre un exemple d'une planche d'une partie de la spécification formelle d'une application, selon l'invention. Cette planche 111 décrit un schéma en bloc d'opérations mathématiques et logiques comprenant cinq blocs ou opérateurs B1-B5. Le premier bloc B1 symbolise une 25 opération de soustraction entre deux entrées numériques NE1 et NE2, le deuxième bloc B2 symbolise une opération de valeur absolue, le troisième bloc B3 représente une opération d'interpolation, le quatrième bloc B4 représente une opération de comparaison et finalement, le cinquième bloc B5 représente une opération de « ou » logique. Ainsi, cette planche 111 montre que les deux entrées numériques NE1 et NE2 30 sont d'abords soustraites (NE1-NE2) dans le premier bloc B1. Ensuite, la valeur absolue du 3056782 9 résultat de la soustraction NDIFF est calculée par le bloc B2 qui délivre en sortie le résultat NDELTA. La valeur absolue NDELTA est interpolée par le bloc B3 sur la base d'une table d'interpolation pré-calculée NTABLE_1 et la valeur numérique du résultat NCRIT est délivrée à la sortie du bloc B3. Ensuite, le bloc B4, compare la valeur numérique NCRIT à un 5 seuil NLEVEL prédéterminé. Finalement, le bloc B5 réalise une opération OU entre le booléen résultant de la comparaison à la sortie du bloc B4 et une entrée booléenne BFORCE et génère ensuite la sortie BCOMMAND de la planche. Conformément à l'invention, la représentation graphique de la planche 111 sera automatiquement transformée par l'analyseur 5 en un code applicatif 9 correspondant 10 en codant chacun des symboles B1-B5 par un code-opération correspondant suivi d'un nombre prédéterminé de codes-paramètres (i.e. codes entrée-sortie). Dans la suite, on considère que le code applicatif est un code octal (ou bytecode) dans lequel chaque code-opération et chaque code-paramètre sont représentés par un mot d'un octet sachant bien entendu, comme décrit précédemment, que chaque mot peut être représenté par un autre 15 nombre de bits. Plus particulièrement, l'analyseur 5 est configuré pour générer le format de mots associés à chaque symbole en minimisant autant que possible les arguments ou paramètres des symboles en considérant certains paramètres comme implicites lorsqu'il n'existe aucune ambigüité. L'analyseur 5 est configuré également pour définir une logique 20 d'enchainement de mots associés à chaque symbole. Chaque instruction commence par le code-opération qui détermine la nature de l'instruction suivi éventuellement par un nombre variable de mots qui identifient chacun un paramètre explicite d'entrée ou de sortie. Par exemple, le premier opérateur ou symbole B1 représentant une opération 25 de soustraction comporte deux entrées El et E2 et une sortie S1=E1-E2. Ainsi, l'analyseur transforme le premier opérateur B1 en quatre octets constitués d'un octet pour le code-opération de soustraction suivi dans l'ordre de trois octets pour identifier les paramètres d'entrées ou opérandes El, E2 et le paramètre de sortie Si. Ceci est alors exprimé dans l'ordre par DIFF NE1 NE2 NDIFF qui se traduit en 01H 01H 02H 03H avec l'opération de 3056782 10 soustraction codé par 01H, la première entrée NE1 par 01H, la deuxième entrée NE2 par 02H, et la sortie NDIFF par 03H. Le deuxième opérateur ou symbole B2 représentant la valeur absolue comporte une entrée E11 et une sortie S11=ABS(S1) qui normalement correspondent à 5 trois octets (l'opération, l'entrée et la sortie). Toutefois, l'entrée et la sortie sont avantageusement considérées comme des paramètres implicites et par conséquent, le deuxième opérateur B2 est codifié sans aucune ambiguïté en un seul octet permettant ainsi de diminuer la taille du code et le nombre d'arguments à traduire. Le troisième opérateur ou symbole B3 représentant une opération 10 d'interpolation comporte deux entrées E21 et F1 ainsi qu'une sortie S21=F(F1, E21). Toutefois, l'entrée F1 correspond à un pointeur qui pointe de manière déterminée sur les variables d'une table calculée préalablement et donc il n'est pas nécessaire de le coder de manière explicite. On notera que tout paramètre qui n'est utilisé qu'une fois dans la spécification (par exemple, F1), peut être placé en mémoire selon l'ordre d'utilisation et 15 par conséquent, il n'est pas nécessaire de spécifier ce genre de paramètres explicitement. Le troisième opérateur B3 est alors codé par seulement trois octets (au lieu de quatre) constitués d'un octet définissant l'opération suivi par un octet définissant l'entrée E21 et un autre octet définissant la sortie S21. Dans un cas particulier dans lequel l'entrée E21 est implicite (car elle correspond à la sortie de l'opérateur précédent B2) et la sortie S21 est 20 implicite (car elle correspond à l'entrée de l'opérateur suivant B4), l'opérateur B3 peut être codé sur un seul octet. Le quatrième opérateur ou symbole B4 représentant une opération de comparaison comporte deux entrées E31 et E32 et une sortie S31 = E31 E32. Dans ce cas, l'analyseur transforme ce quatrième opérateur B4 en quatre octets constitués d'un octet 25 pour le code-opération d'inégalité suivi dans l'ordre de trois octets pour identifier les paramètres d'entrées E31, E32 et le paramètre de sortie S31. Finalement, le cinquième opérateur ou symbole B5 représentant une opération de « OU » logique comporte deux entrées E41 et E42 et une sortie S41=E41 OR E42. Dans ce cas, l'analyseur transforme ce cinquième opérateur B5 en quatre octets constitués d'un 30 octet pour le code-opération OU suivi dans l'ordre de trois octets pour identifier les 3056782 11 paramètres d'entrées E41, E42 et le paramètre de sortie S41. On peut éventuellement considérer que la dernière donnée booléenne produite (i.e. le résultat de la comparaison) soit une sortie implicite du code-opération OU. Dans ce cas, on utilise un code spécifique pour cet opérateur afin de spécifier que sa sortie est implicite. 5 Ainsi, l'analyseur prend en entrée la représentation graphique de la planche et produit automatiquement en sortie un code applicatif correspondant avec un format particulier de la manière suivante : ## Codes opérations SUB = 01h 10 ABS = 02h F = 03h COMPARE 04h OR = 05h 15 ## Codes des variables de type booleens BDECISION = 01h BFORCE = 02h BCOMMAND = 03h 20 ## Codes des variables de type flotant double précision. NE1 = 01h NE2 = 02h NDIFF = 03h NDELTA = 04h 25 NCRIT = 05h NLEVEL = 06h ## Byte code généré. # NDIFF := NE1 - NE2 30 01h 01h 02h 03h # NDELTA := ABS(NDIFF) 02h 03h 04h # NCRIT := F(NTABLE_1,NDELTA) 03h 04h 05h # BDECISION := NCRIT >= NLEVEL 04h 05h 06h 01h # BCOMMAND := BDECISION OR BFORCE 3056782 12 05h 01h 02h 03h Ce code ci-dessus comporte 18 octets, qu'on peut réduire davantage (par exemple à seulement 10 octets) en utilisant des passages de paramètres implicites et en 5 définissant des nouveaux code-opérations : # * := NE1 - NE2 11h 01h 02h # * := ABS(*) 10 22h # * := F(NTABLE_1,*) 23h 15 # * := * >= NLEVEL 24h 06h # BCOMMAND := * OR BFORCE 35h 02h 03h 20 Ceci permet d'avoir un gain proche de « 2 », à la fois sur le temps de chargement du code depuis la mémoire et sur le temps de décodage des paramètres. A l'étape E3 (Fig. 2), l'interpréteur 13 ainsi que le code applicatif 9 spécifique à l'application sont embarqués dans un processeur 15. 25 Le processeur 15 comporte en général plusieurs coeurs numériques 17 pouvant fonctionner simultanément de manière autonome ainsi que plusieurs mémoires internes Ml, M2, M3 généralement utilisées en tant que mémoires caches afin d'en maximiser l'utilisation (i.e. une même cellule de mémoire peut servir consécutivement à différentes données durant les traitements où elles sont les plus fréquemment utilisées). 30 La Fig. 4 illustre de manière schématique une partie fonctionnelle d'un coeur numérique d'un processeur, selon l'invention. Chaque coeur numérique 17 comporte des unités d'exécution 171-179 destinées à faire des calculs sur des nombres entiers 171 et réels (ou flottant) 173, à accéder 175 à des mémoires internes M1-M3 pour les instructions propres du processeur, 35 à accéder 177 à des mémoires internes M1-M3 pour des données, à faire des opérations 3056782 13 de décodage 179 d'instruction, à prendre des décisions de branchement, etc. Les mémoires caches M1-M3 sont organisées en plusieurs niveaux du plus rapide mais plus petit vers le plus lent mais plus gros. Les caches sont souvent dimensionnées pour servir efficacement plusieurs coeurs à la fois, en particulier tous les coeurs à la fois. 5 A titre d'exemple, les mémoires caches M1-M3 peuvent être organisées en trois niveaux. La mémoire cache M1 de premier niveau (dite L1) est ultra rapide mais de faible taille (par exemple de l'ordre de 32 koctets de code et 32 koctets de données). La mémoire cache M2 de deuxième niveau (dite L2) est moins rapide mais de taille plus élevée (par exemple de l'ordre de 256 koctets). La mémoire cache M3 de troisième niveau (dite 10 L3) est la moins rapide mais la plus grosse en taille. Les mémoires caches permettent d'accélérer l'exécution d'un programme. Le processeur 15 dispose aussi d'un plan mémoire principal 19 de très grande taille de type accès à double vitesse DDR (Double Data Rate) mais dont les accès sont plus lents que tous les niveaux des mémoires caches M1, M2 et M3. 15 Ainsi, pour profiter de la rapidité des mémoires caches M1-M3, l'interpréteur 13 est prioritairement chargé en mémoire rapide suivi par les données (constates et variables). En effet, la partie de la mémoire cache M1 de premier niveau L1 consacrée aux instructions M1a est utilisée massivement pour loger l'interpréteur 13 qui présente une taille très compacte lui permettant cette possibilité. La partie de la mémoire cache M1b 20 consacrée aux données temporaires est utilisée pour stocker les piles de registres et les variables sachant que la gestion sous forme de piles autorisée par la solution de la présente invention permet ce type d'utilisation très performante. Dans le cas où la taille de la mémoire cache M1 serait insuffisante, une partie des piles de registres et des variables pourra être stockées dans la mémoire cache M2 de deuxième niveau L2. 25 Le code applicatif 9 étant très compact, peut être chargé en mémoire plus lente (par exemple dans la mémoire principale DDR) dans la mesure où il est possible d'anticiper son chargement en mémoire rapide avant qu'il ne soit requis. Finalement, les mémoires caches de plus haut niveau (par exemple, L3) qui sont habituellement partagés, sont à privilégier pour les échanges entre les coeurs et l'extérieur. 3056782 14 A l'étape E4 (Fig.2), le code applicatif 9 est exécuté par le processeur 15. En particulier, le code applicatif 9 devient comme une simple table de configuration décodée au fil de l'eau par le processeur 15 embarqué. En particulier, l'interpréteur 13 lit le code courant associé à un symbole visé, il 5 en déduit le nombre et le type de paramètres à lire, il trouve les pointeurs associés aux paramètres dans les codes d'entrées-sortie des paramètres, et il exécute le code associé au symbole visé. On notera que les données vont être consommées dans le même ordre que l'exécution des symboles d'où le fait que certains paramètres peuvent être implicites (i.e. rémanents). Ainsi, on n'a pas besoin de donner des informations pour savoir quel 10 symbole va utiliser quel rémanent. Avantageusement, l'interpréteur 13 est configuré pour s'alimenter par anticipation de phase (dite prefetch) des éléments du code applicatif 9 stocké dans une mémoire interne ou externe. En effet, l'interpréteur 13 peut aller lire en avance le code applicatif 9 depuis la mémoire interne M2 ou M3 ou éventuellement depuis la mémoire 15 externe 19. Cette anticipation de lecture permet de masquer les temps d'accès vers le code applicatif avec un gain supplémentaire d'efficacité. L'interpréteur 13 et le code applicatif 9 généré peuvent avantageusement être intégrés dans un calculateur avionique en particulier, pour des fonctions applicatives de type control, asservissement et logiques opérationnelles. Ceci permet l'utilisation efficace 20 de plus de coeurs ce qui n'est pas possible dans l'état de l'art où les besoins de chaque coeur saturent significativement la mémoire. Une autre conséquence évidente en sera une plus forte intégration des calculateurs avioniques et/ou une plus grande capacité d'accueil de fonctions avioniques plus gourmandes en puissance CPU. Bien entendu, l'interpréteur et le code applicatif 25 peuvent également être intégrés dans d'autres types de dispositifs qui peuvent être embarqués dans des satellites, des trains ou autres véhicules, des bateaux, etc. Par ailleurs, on notera que le système et procédé de la présente invention permet de diviser la taille du code exécutable par un facteur d'environ 10 par rapport à l'art antérieur, ce qui favorise notablement le temps de démarrage dans la plupart des 3056782 15 coeurs numériques et facilite l'utilisation de certains coeurs numériques (par exemple la gamme auto-motive). En outre, la diminution du taux d'utilisation du plan mémoire principal au bénéfice d'une plus forte utilisation des plans mémoires caches ultra-rapides se traduit au 5 final par une bien meilleure efficacité d'utilisation des coeurs numériques des processeurs. Les gains obtenus dépendent entre autres de la taille des symboles élémentaires. De plus, la diminution du taux d'utilisation du plan mémoire principal et une meilleure caractérisation temporelle des accès mémoires permettent d'envisager l'utilisation de plusieurs coeurs numériques en parallèles sur « un système sur une puce » 10 SoC (System on a Chip) multi-coeurs. L'utilisation de plusieurs coeurs numériques permet une multiplication de la performance offerte par le SoC mufti-coeurs. En outre, la meilleure caractérisation du comportement (vis-à-vis des accès mémoires) du code applicatif est un facteur très favorable à la détermination du pire cas de temps d'exécution logiciel applicatif. 15 Par ailleurs, la présente invention n'utilise pas de compilateurs du commerce et permet une meilleure maitrise du comportement du code applicatif ce qui est un facteur favorable à la certification. On notera aussi que le contrôle des instructions selon l'invention permet d'appliquer toute règle contribuant à un usage équitable et optimal des ressources bus et 20 mémoires du processeur. Finalement, le système et procédé de la présente invention s'applique aux processeurs aussi bien mono-coeur que multi-coeurs, ainsi qu'aux processeurs qui utilisent des plans mémoires internes rapides. REVENDICATIONS1. Système de génération d'un code applicatif exécutable par un processeur à partir d'une spécification formelle (11) associée à une application, ladite spécification formelle comprenant des opérateurs (B1-B3), caractérisé en ce que ledit système comporte un analyseur (5) configuré pour coder chaque opérateur de ladite spécification formelle par un code-opération correspondant suivi d'un nombre minimal de code(s)-entrée(s) et code-sortie identifiant des paramètres d'entrées et de sortie associés audit opérateur, générant ainsi automatiquement un code applicatif (9) compact adapté pour être stocké dans une mémoire associée audit processeur (15) et pour être exécuté par un interpréteur (13) stocké dans une mémoire du processeur. 2. Système selon la revendication 1, caractérisé en ce que l'analyseur (5) est configuré pour définir comme implicite au moins un des paramètres d'entrées et de sortie de chaque symbole appartenant à un sous-ensemble de symboles spécifiques. 3. Système selon la revendication 1 ou 2, caractérisé en ce que le code applicatif (9) est un code dans lequel chaque code-opération et/ou chacun des code(s)-entrée(s) et code-sortie sont représentés par un champ de bits prédéterminé. 4. Système selon l'une quelconque des revendications précédentes, caractérisé en ce que le code applicatif (9) est un code octal, dans lequel chaque code-opération et/ou chacun des code(s)-entrée(s) et code-sortie sont représentés par un octet ou un multiple d'octets. 5. Système selon l'une quelconque des revendications précédentes, caractérisé en ce que la spécification formelle est une représentation graphique formelle. 6. Système selon l'une quelconque des revendications précédentes, caractérisé 30 en ce que ledit interpréteur (13) est configuré pour être stocké en totalité ou au moins en 25 3056782 17 partie dans une mémoire cache de premier niveau (L1) du processeur (15), ledit interpréteur étant adapté pour décoder et exécuter les instructions du code applicatif (9) au fur et à mesure de leur lecture. 5 7. Système selon la revendication 6, caractérisé en ce que l'interpréteur (13) est configuré pour lire chaque code-opération courant, pour déduire le nombre et le type de paramètres, pour trouver des pointeurs associés auxdits paramètres, pour déterminer des spécifications implicites, et pour exécuter le code-opération courant. 10 8. Système selon la revendication 6 ou 7, caractérisé en ce que l'interpréteur (13) est configuré pour s'alimenter par anticipation de phase des éléments du code applicatif stocké dans une mémoire interne ou externe. 9. Calculateur avionique comportant un processeur intégrant un interpréteur 15 et un code applicatif généré par le système selon l'une quelconque des revendications précédentes. 10. Procédé de génération d'un code applicatif exécutable par un processeur à partir d'une spécification formelle associée à une application, ladite spécification formelle 20 comprenant des opérateurs, caractérisé en ce que ledit procédé comporte les étapes suivantes : - générer automatiquement un code applicatif compact en codant chaque opérateur de ladite spécification formelle par un code-opération correspondant suivi d'un nombre minimal de code(s)-entrée(s) et/ou code-sortie identifiant des paramètres d'entrées et de sortie associés audit opérateur, stocker ledit code applicatif dans une mémoire associée à un processeur, et exécuter ledit code applicatif par un interpréteur stocké dans une mémoire du processeur.