Brevet FR2917522A1 — publié le 20081219

couverture suffisante. Une démarche par objectif de test n'est donc pas appropriée pour réaliser du test de non-régression lors de l'ajout, suppression ou remplacement d'un composant d'un système puisque la définition d'objectifs de test n'offre a priori aucune garantie quant à la couverture du composant concerné. Les tests structurels sont quant à eux en général limités à des couvertures rudimentaires comme la couverture de branches où chaque transition doit être exécutée une fois, sachant que les couvertures plus complexes comme la couverture de chemins où toutes les séquences de transitions doivent être exécutées au moins une fois, chaque 1 o séquence de transition représentant un comportement, ne sont en général pas atteignables, toujours à cause de l'explosion combinatoire. Ceci est très gênant, car par exemple dans le cas d'une boucle, on se contente pour atteindre la couverture de branches, d'exécuter la boucle une fois, alors que dans le cas de la couverture de chemins, il faut exécuter la boucle jusqu'à la 15 sortie de la boucle au moins. Un moyen pour contourner ces difficultés liées à l'analyse de modèles de systèmes d'automates communicants, est l'utilisation des méthodes d'analyses de flots de données et de réduction paramétrée, encore appelée slicing , pour réduire les modèles en amont, c'est-à-dire avant l'exécution 20 des techniques de calculs intensifs. Le slicing est une méthode d'analyse de programmes, qui fut introduite à l'origine par M. Weiser en 1979, dans le but de formaliser et d'automatiser les abstractions mentales que les programmeurs construisent lors de leur activité de débogage. Depuis lors, le slicing a été étendu pour l'appliquer à la réduction et la compréhension 25 de divers formalismes, dans le cadre de problématiques diverses. Un but de l'invention est notamment de permettre de réduire efficacement le graphe sur lequel des analyses formelles peuvent être faites. A cet effet, l'invention a pour objet un procédé de réduction paramétrée d'un modèle M, le modèle M étant l'union de modèles Mi d'automates communicants, et 30 comportant un ensemble T de transitions tr, l'ensemble T étant l'union d'ensembles Ti qui sont des restrictions de l'ensemble T aux modèles Mi, le modèle M est transformé par un mécanisme d'analyse statique en une structure de données sous forme de tableaux d'ensembles de transitions CD[M], DD[M] et ComD[M], pour chaque transition tr les ensembles CD[tr, M], DD[tr, M] et ComD[tr, M] contenant respectivement les transitions qui impactent une transition tr par une relation de dépendance de contrôle, une relation de dépendance de données et une relation de dépendance de communication, un sous-ensemble CRIT du modèle M étant défini, Crit étant l'ensemble des transitions qui appartient au sous-ensemble CRIT, un sous-ensemble Ti' étant la restriction de l'ensemble T à un sous-système Mi, chaque ensemble Ti' contenant pour chaque sous-système Mi toutes les transitions tr qui ont un impact sur les transitions de l'ensemble Crit selon l'une au moins des relations de dépendance précédentes, la restriction Mi' de chaque sous-système Mi étant déduite de chaque ensemble Ti', le modèle réduit M' étant composé de l'ensemble des restrictions Mi'. D'autres caractéristiques et avantages de l'invention apparaîtront à l'aide de la description qui suit faite en regard de dessins annexés qui représentent : la figure 1, une illustration des modèles, initial et réduit, ainsi que des analyseurs entrant en jeu dans la mise en oeuvre du procédé selon l'invention ; la figure 2, une présentation des étapes possibles pour la mise en oeuvre du procédé de réduction paramétrée selon l'invention ; - la figure 3, une présentation du processus permettant d'obtenir un 20 ensemble CD[tr, M] contenant les transitions qui impactent une transition tr par une dépendance de contrôle ; - la figure 4, une présentation du processus permettant d'obtenir un ensemble DD[tr, M] contenant les transitions qui impactent une transition tr par une dépendance de données ; 25 la figure 5, une présentation du processus permettant d'obtenir un ensemble ComD[tr, M] contenant les transitions qui impactent une transition tr par une dépendance de communication ; - les figures 6a et 6b, une illustration d'un exemple d'application du procédé selon l'invention. 30 La figure 1 illustre les modèles, initial et réduit, et analyseurs entrant en jeu dans un procédé de réduction paramétrée 1 appelé par la suite procédé de slicing . Un système auquel s'applique l'invention utilise notamment l'analyse de 35 modèles de type processus ou automates communicants qui sont généralement basés sur des systèmes de transitions étendus représentant les automates avec des communications par rendez-vous synchrones. Les formalismes les plus connus sont notamment EIOLTS, acronyme de l'expression anglo-saxonne extended input output labelled transition systems ou IOSTS, acronyme de l'expression anglo-saxonne input output symbolic transition systems . Pour le formalisme de communication EIOLTS extended implique que des données peuvent être utilisées, de façon optionnelle. Dans le cas où des communications asynchrones, par exemple des files d'attentes de type FIFO ou LIFO, seraient envisagées, ces communications peuvent toujours être représentées dans les formalismes cités précédemment en utilisant des processus qui gèrent la communication. Les communications sont ou non porteuses des données. Une spécification formée d'automates communicants, ou modèle, est un ensemble de sous-systèmes de transition qui peuvent être dits atomiques , c'est-à-dire non décomposables eux-mêmes en sous-systèmes, communiquant entre-eux par des canaux de communication qui décrivent des possibilités de rendez-vous entre transitions de sous-systèmes distincts. Un système de transitions étendues atomique est alors un ensemble d'actions, ou transitions. Chaque transition comporte notamment : un état source ; un état cible ; - une garde logique qui porte sur les variables du système, conditionnant l'exécution de la transition ; une communication (entrée ou sortie), non obligatoire ; - des affectations sur les variables qui sont effectuées par des fonctions sur ces variables. L'entrée d'une transition peut mettre à jour une variable du système par acquisition d'une donnée. Une expression fonction des variables du système peut être mise en sortie. Le système atomique comporte un état initial qui est l'état de départ du système en cas d'exécution. Dans la sémantique retenue, chaque transition est exécutable si le système est dans son propre état source. Son exécution est alors conditionnée par sa garde et par son entrée s'il y en a une. Elle provoque la mise à jour des variables par ses propres affectations et éventuellement une sortie s'il y en a une. Enfin le système se trouve à l'issu de cette exécution dans l'état cible de la transition. Un chemin maximal est une séquence d'exécution de transitions soit infinie, soit finie et qui ne peut être prolongée. Un chemin maximal, si le système est fini, est donc soit un chemin qui se termine par une boucle, a priori finie, soit par un blocage, sans suite possible. La figure 1 montre un modèle M 2 qui représente un système comme entrée du procédé d'analyse par slicing 1. Son pendant est un modèle M' 3 qui est la sortie du procédé et qui représente le modèle réduit par le procédé de slicing . Le modèle M est transformé par un mécanisme d'analyse syntaxique en une structure de données interne. Cette structure de données est transmise à différentes fonctions spécialisées en fonction du type d'analyse requise. Une autre entrée de ces fonctions est un critère de slicing 4 qui est un sous-ensemble du modèle sur lequel va être ciblée l'analyse. Ce critère de slicing nommé CRIT est soit entré par un utilisateur directement sous forme de sous-ensemble du modèle M, soit déduit du contexte d'analyse, notamment de propriétés à prouver dans le cas d'utilisation du procédé pour la preuve des propriétés. Le CRIT peut être considéré comme une sélection de transitions, le processus de slicing permettant de vérifier si ces transitions sont mises en jeu pour une application donnée, dont dépend le critère de slicing . Trois types d'analyses sont avantageusement utilisés. Ces analyses sont l'analyse par dépendance de contrôle 5, l'analyse par dépendance de données 6 et l'analyse par dépendance de communication 7. L'analyse par dépendance de contrôle est notamment décrite dans l'article de V.Ranganath, T.Amtoft, A.Banerjee, M.Dwyer et J.Hatcliff A new foundation for control-dependance and slicing for modern program structures In European Symposium on Programming (ESOP), pages 77-93, 2005. L'analyse par dépendance de données est notamment décrite dans l'ouvrage de F.Nielson, H.Nielson et C.Hankin Principles of Program Analysis Springer-Verlag, 1999. L'analyse par dépendance de communication est notamment décrite dans l'article de L.Millett et T.Teitelbaum Issues in slicing promela and its applications to model checking, protocol understanding and simulation Software Tools for Technology Transfer (STTT), 2(4), pages 343-349, 2000. Nous décrivons une méthode pour réaliser ces trois analyses en prenant en compte les caractéristiques des spécifications formées d'automates communicants : ces trois analyses peuvent être contenues dans trois modules 5, 6, 7 utilisés par le procédé de slicing 1 et pourront par la suite être nommés respectivement CD, DD et COM. Les trois modules de traitement CD, DD et COM produisent chacun des résultats CD[M], DD[M] et ComD[M] qui sont des structures de données, telles que des tableaux d'ensembles de transitions, directement utilisables par le processus principal décrit par la suite relativement à la figure 2, ce processus intégrant ces résultats pour produire le modèle réduit M', sous-ensemble du modèle M et résultat du procédé. La figure 2 illustre des étapes possibles pour la mise en oeuvre d'un procédé de réduction paramétrée ou slicing 1 selon l'invention. Des résultats CD[M], DD[M], ComD[M] sont calculés respectivement à l'aide des modules CD, DD et COM. Ces résultats sont des structures de données directement utilisables par le module principal 1 qui va intégrer ces résultats et produire le modèle M' qui est un sous-ensemble du modèle M et résultat de tout le procédé. Les structures de données peuvent être des tableaux d'ensembles de transitions. Le mécanisme d'intégration est notamment décrit par les étapes suivantes. Dans une étape préliminaire 20, les modules analyseurs CD, DD et COM permettent de calculer, pour chaque transition tr du modèle M, les trois ensembles CD[tr, M], DD[tr, M], ComD[tr, M]. Ces ensembles contiennent les transitions qui impactent la transition tr par une dépendance de contrôle 5, de données 6 ou de communication 7. Ces structures de données sont adaptées pour la réduction paramétrée en arrière , calculant de façon récursive l'ensemble des transitions dont les transitions du critère dépendent. Plus précisément, il s'agit de trouver les transitions pour lesquelles il existe une séquence de dépendances qui ne comprend pas plus d'une dépendance de communication consécutivement, et qui mène à une transition du critère. De façon duale, un procédé de réduction en avant calcule l'ensemble des transitions qui dépendent des transitions du critère. Par la suite le procédé de réduction en arrière est décrit plus en détail, sachant que le procédé de réduction en avant est implanté de façon similaire une fois que les structures de données CD[tr, M], DD[tr, M] et ComD[tr, M] sont adaptées. Les ensembles CD[tr, M], DD[tr, M] et ComD[tr, M] sont intégrés par un processus dont l'objectif est notamment de calculer tout ce qui impacte une transition de l'ensemble CRIT 4 par l'un des trois critères de dépendance de contrôle 5, de données 6 ou de communication 7. L'ensemble de toutes les transitions est déduit du modèle interne directement et est noté T. On note Crit l'ensemble des transitions qui appartiennent au sous-ensemble CRIT du modèle M. T étant l'union des sous-ensembles Ti qui sont les restrictions de T à chaque automate Mi, ou sous-système atomique Mi, du modèle M, il en est de même pour l'ensemble Crit qui est un sous-ensemble de T par définition, et qui est alors l'union des sous-ensembles Ti', restrictions de Crit à chaque sous-système Mi. Dans une étape suivante d'initialisation 20', un ensemble de travail, qui pourra être nommé worklist par la suite, est constitué. Il est initialisé par l'union des sous-ensembles Ti' donc il contient à ce stade toutes les transitions de l'ensemble Crit. Pour s'assurer que les séquences de dépendances qui comprennent plusieurs dépendances de communication consécutives ne sont pas prises en compte, le procédé utilise des Booléens notés done[tr] et ViaCom[tr]. Pour chaque transition tr, done[tr] est vrai si le traitement de la transition tr est terminé, et ViaCom[tr] est vrai si le traitement de la transition tr a été atteint seulement via une dépendance de communication. done[tr] et ViaCom[tr] sont initialisés à l'état faux . Le procédé forme par la suite une boucle 11, appelée boucle principale, et qui commence à une première étape 21 de test. Si worklist n'est pas vide, on extrait 211 un élément de l'ensemble worklist que l'on nomme tri. Sinon, on termine 212 la boucle principale. Le processus de réduction étant terminé, on rétablit l'atteignabilité (cf. ci-après) dans les sous-ensembles Mi' et on en déduit le modèle réduit M', les sous-ensembles Mi' étant définis par la suite lors de la description de la boucle principale. Par la suite une transition tr n'est traitée que si done[tr] est faux.35 Dans une étape suivante 22, pour chaque transition tr des ensembles CD[trl, M] ou DD[trl, M] cette transition tr est insérée dans worklist, les ensembles CD[trl, M] et DD[trl, M] étant les ensembles de transitions qui impactent la transition tri respectivement par une dépendance de contrôle 5 et une dépendance de données 6. Si de plus viaCom[tr] est faux et tr appartient à un sous-ensemble Ti, alors tr est ajouté au sous-ensemble Ti'. Puis viaCom[tr] est positionné à faux et done[tr] est positionné à vrai. Dans une étape suivante 23, pour chaque transition tr dans ComD[trl] telle que viaCom[tr] et viaCom[trl] sont faux, la transition tr est insérée dans worklist. Si de plus la transition tr appartient à un sous-ensemble Ti, alors elle est ajoutée au sous-ensemble Ti'. Puis viaCom[tr] est positionné à vrai. L'élément tri étant retiré de worklist, le procédé retourne à la première étape 21 de la boucle 11. La boucle principale qui a démarré à cette étape 21 se termine lorsque les ensembles de transitions Ti' ont été construits avec succès conformément aux étapes précédentes. Chaque ensemble Ti' contient pour chaque automate Mi appartenant au modèle M toutes les transitions qui ont un impact sur les transitions du sous-ensemble CRIT. Le procédé déduit de chaque Ti' la restriction Mi' de Mi aux transitions de Ti' et donc également le modèle réduit M', l'ensemble des Mi', et sous-ensemble du modèle M. Il peut arriver que des transitions de M', qui étaient atteignables dans M, ne sont plus atteignables dans M'. Le procédé selon l'invention propose dans ce cas de rétablir l'atteignabilité de manière adaptée à l'utilisation qui sera faite du résultat de la réduction. Par exemple, dans le cas de l'utilisation du procédé pour la preuve de propriétés, le rétablissement de l'atteignabilité peut être obtenu par un calcul inspiré de la méthode de tau-réduction, bien connue dans le contexte des systèmes de transitions étiquetés. A la base, il s'agit dans ce cas d'assimiler les transitions présentes dans le modèle M et non présentes dans le modèle M' à des transitions tau, puis de regrouper les séquences de transitions tau en une seule transition tau. Une fois l'atteignabilité rétablie, M' forme le résultat final de l'analyse. La figure 3 illustre le processus qui permet d'obtenir l'ensemble CD[tr, M]. 35 Etant donné un automate Mi dans le modèle M, on note Ti l'ensemble des transitions de Mi. Dans une étape d'initialisation 30, on commence par construire l'ensemble des transitions conditionnelles de Mi, les transitions ayant une garde non triviale, c'est-à-dire non égale à vrai pour tout paramétrage. Cet ensemble est noté conds[Mi]. Puis on initialise les ensembles CD[tr, Mi] à l'ensemble vide, pour toutes transitions tr dans Mi, CD[tr, Mi] étant l'ensemble des transitions de Mi qui impactent la transition tr par une dépendance de contrôle. Pour chaque état s dans Mi et chaque transition trc dans conds[Mi], on définit un ensemble P[s, trc] qui est l'ensemble des chemins maximaux dans Mi qui commencent par trc et contiennent s. Pour mémoire, un chemin est dit maximal s'il n'est contenu dans aucun chemin plus grand. Cet ensemble est d'abord initialisé par l'ensemble vide, qui ne contient aucun élément. Un ensemble de travail worklist est également créé et initialisé à vide. Pour chaque élément trc de conds[Mi] et pour chaque transition successeur immédiat de trc, c'est-à-dire dont l'état source est égal à l'état cible de trc, notée trs, on considère l'ensemble des chemins maximaux que trc initie et qui contiennent trs. Ces chemins sont alors ajoutés à des ensembles P[source(trc), trc] et P[cible(trc), trc] eux-mêmes en construction. Pour toute transition t, source(t) et cible(t) sont respectivement l'état source et l'état cible de la transition t. Ensuite chacune des transitions conditionnelles est ajoutée à l'ensemble de travail worklist. Le processus opère en boucle à partir d'une première étape 31. Dans cette étape on commence par effectuer un test 310 sur worklist. Si worklist n'est pas vide, on extrait 311 une transition de l'ensemble worklist, nommée tri. Sinon on termine la boucle principale 39. Le processus est alors terminé. Pour tout état s et toute transition conditionnelle trc, on calcule les CD[tr, Mi] en fonction des P[s, trc] comme indiqué par la suite lors de la description de la fin du processus. Dans une étape suivante 32, on effectue un test de jointure 320 sur l'élément tri extrait de worklist. Si cet élément tri est à la jointure de plusieurs chemins, c'est-à-dire si l'ensemble des transitions qui ont le même état source que tri contient plus d'un élément, alors on lance une mise à jour 321 de l'ensemble P[cible(trl), trc] et de worklist, P[cible(trl), trc] étant l'ensemble des chemins maximaux qui partent de trc et passent par l'état cible de tri. Plus particulièrement, si plusieurs transitions ont cible(tr) pour état cible, alors pour chaque état s tel qu'au moins une transition conditionnelle a s pour état source : - si toutes les transitions conditionnelles tr qui ont s pour état source sont telles que P[cible(trl), tr] et succs[tr, Mi] ont le même nombre d'éléments, P[cible(trl), tr] et succs[tr, Mi] étant respectivement l'ensemble des chemins maximaux qui partent de tr et passent par l'état cible de tri et l'ensemble des successeurs de tr ; alors pour toute transition conditionnelle trc appartenant à conds[Mi] différente de trl, si la différence de l'ensemble P[s, trc] avec l'ensemble P[cible(trl), trc] est non vide, autrement dit si l'ensemble P[s, trc] contient des éléments que P[cible(trl), trc] ne contient pas, ces éléments sont ajoutés à l'ensemble P[cible(trl), trc] et tous les successeurs de tri sont ajoutés à l'ensemble de travail worklist, conds[Mi] étant l'ensemble des transitions qui ont une garde non triviale. Par la suite, à la fin de cette étape 32, on effectue un test 322 sur le nombre de successeurs de la transition tri. Dans le premier test 320, si tri ne forme pas une jointure de chemins, on vient directement à ce deuxième test 322 tester son nombre de successeurs. Si l'élément tri a un seul successeur, appelé trs, on met à jour 33 l'ensemble P[cible(trs), trc] à partir de P[cible(trl), trc]. Plus particulièrement, si tri a un seul successeur: - alors pour toutes transitions conditionnelles trc de conds[Mi] ; si la différence de l'ensemble P[cible(trl), trc] et de l'ensemble P[cible(trs), trc] est non vide, autrement dit si l'ensemble P[cible(trl), trc] contient des éléments que P[cible(trs), trc] ne contient pas, ces éléments sont ajoutés à l'ensemble P[cible(trs), trc] et trs est ajouté à l'ensemble de travail worklist. La transition tri est retirée de worklist, puis le processus reprend à la première étape 31 plus particulièrement sur le test 310 de worklist. Si le test de succession 322 n'indique pas que tri a un seul successeur, le processus revient de même au test 310 de la première étape. A partir de ces tests 310, le processus en boucle continue. Il se termine par une dernière étape 39 lorsque worklist devient vide. Dans cette dernière étape 39, pour tout état s de Mi et pour toute transition trc ayant une garde non triviale, appartenant donc par définition à conds[Mi], si P[s, trc], ensemble des chemins maximaux qui partent de trc et qui contiennent s : - contient le même nombre d'éléments que succs[trc, Mi] ; - et s'il existe une transition trc' de conds[Mi] qui a le même état source que trc et telle que P[s, trc'] ait moins d'éléments que succs[trc', Mi] ; alors il existe un chemin depuis trc' qui crée une dépendance de contrôle de trc sur toutes les transitions tr dont l'état source est s ; on ajoute alors trc à l'ensemble CD[tr, Mi] en construction pour toutes ces transitions tr. Le module CD 5 est appelé pour chaque Mi dans le modèle M. Les ensembles CD[tr, Mi] sont alors construits et disponibles pour être intégrés par le premier processus, illustré par la figure 2, dans CD[M]. La figure 4 illustre le processus qui permet d'obtenir l'ensemble DD[tr, M]. Etant donné un automate Mi dans le modèle M, on note Ti l'ensemble des transitions de Mi. On définit les structures de données nécessaires à la mise en oeuvre du processus dans une étape préliminaire d'initialisation 40. On définit deux tableaux Def et Ref d'ensembles de variables, indicés par les éléments de Ti. On définit par ailleurs trois tableaux Gen, Kill et RD d'ensembles de définitions, sachant qu'une définition est un couple (tr, v) formé d'une transition tr et d'une variable v, ces tableaux étant aussi indicés par les éléments de Ti. On définit aussi deux ensembles de travail, un ensemble appelé newinfo qui est un ensemble de définitions et un ensemble worklist qui est comme dans les processus précédents un ensemble de transitions. Pour chaque transition tr de Ti, on initialise : Def[tr] par l'ensemble des variables, soit mises à jour par l'entrée de tr si elle existe, soit mises à jour par une affectation de tr ; Ref[tr] par l'ensemble des variables qui sont soit transmises par une sortie de tr à l'extérieur de l'automate qui contient tr, soit présentes dans la garde de tr, soit utilisées dans un terme qui est affecté à une variable, tel que le résultat ne soit pas l'identité sur cette variable ; - RD[tr] et DD[tr] par l'ensemble vide ; Gen[tr] par l'ensemble des couples (tr, v) où v appartient à Def[tr] ; Kill[tr] par l'ensemble des couples (trk, v) où trk est une transition quelconque de Ti différente de tr et où v appartient à Def[tr] ; - Worklist par l'ensemble Ti. Une fois l'initialisation achevée, un processus en boucle s'engage par une première étape 41. Cette étape commence par un test 410 sur workiist. Si worklist n'est pas vide, on extrait 411 un élément de l'ensemble worklist que l'on nomme tri. Dans le cas contraire on termine la boucle principale en passant à la dernière étape 49 qui sera décrite par la suite. Dans une étape suivante 42, l'ensemble newinfo étant initialisé à vide, pour toute transition trp prédécesseur de tri, c'est-à-dire dont l'état cible est égal à l'état source de tri, on ajoute 421 à l'ensemble newinfo tous les éléments de RD[trp] sauf ceux qui appartiennent aussi à Kill[trp], et on ajoute également à newinfo les éléments de gen[trp]. Puis on réalise un test 422 sur l'ensemble newinfo. Si newinfo contient l'ensemble RD[trI] strictement, c'est-à-dire qu'il y a dans newinfo des éléments en plus de ceux de RD[trI] alors on ajoute 423 ces éléments à RD[trI], puis on ajoute 424 les successeurs trs de tri à l'ensemble worklist. Enfin, on retire tri de worklist. Le processus se reboucle sur la première étape 41, au niveau du test 410 de worklist. Si le test 422 sur l'ensemble newinfo est négatif, c'est-à-dire si RD[trI] n'est pas strictement inclus dans newinfo, alors le processus se reboucle aussi sur la première étape 41 au niveau du test 410 de worklist. Une fois que worklist est vide, le processus se termine par la dernière étape 49. Dans cette étape, pour chaque transition tr de Ti, et pour chaque élément (trk,v) de RD[tr] : - si la variable v est utilisée dans la garde de tr ; ou si la variable v appartient à Ref[tr] mais n'est pas affectée par 30 l'entrée de la transition, si elle existe ; - alors on ajoute trk à l'ensemble DD[tr, Mi] ainsi construit. Enfin le module DD 6 est appelé pour chaque Mi dans le modèle M. Les ensembles DD[tr, Mi] sont alors construits et disponibles pour être intégrés par le premier processus, illustré par la figure 2, dans DD[M]. 35 La figure 5 illustre le processus qui permet d'obtenir l'ensemble ComD[tr, M]. Dans une étape préliminaire non représentée, on définit les structures de données nécessaires à la mise en oeuvre du processus. L'ensemble des canaux de communication du système est noté C. Les ensembles des canaux du système indicés comme les automates Mi du système sont notés Ci et l'union de ces ensembles de canaux est par définition l'ensemble C. emit et rcv sont deux tableaux d'ensembles de transitions indicés par les éléments de C. Enfin le tableau où est stocké le résultat, qui est un tableau d'ensembles de transitions noté ComD[tr, M], est initialisé à vide. Le processus comporte deux boucles ou deux étapes principales 51, 52. Une première boucle 51 permet de calculer les éléments de emit et de rcv. A cet effet, pour toute transition tr de T, où T est l'ensemble des toutes les transitions du modèle M : - si tr appartient à Ti, avec les notations précédentes, Ti étant 15 l'ensemble des transitions du ième automate du système ; si tr a une entrée, ou une sortie, et que cette entrée, ou cette sortie, correspond à celle du canal c de Ci ; - alors elle est ajoutée à l'ensemble emit[c] s'il s'agit de l'entrée ou à l'ensemble rcv[c] s'il s'agit de la sortie. 20 La seconde boucle 52 permet de calculer les dépendances de communications dans le modèle, en se basant sur les informations de emit et rcv. Ainsi, pour tout canal c de C et pour toute transition tre de emit[c], si l'ensemble Ti contient tre, alors pour toute transition trr de rcv[c] : si l'ensemble Tj contient trr ; 25 - et si i est différent de j ; - alors on ajoute tre à ComD[trr, M] et on ajoute trr à ComD[tre, M]. Le calcul des ensembles ComD[tr, M] est alors achevé et ces ensembles sont renvoyés au processus principal, illustré par la figure 2, pour intégration dans ComD[M]. 30 Un procédé de réduction paramétrée d'automates communicants tel que décrit précédemment peut avantageusement faire l'objet de plusieurs applications. Une première application peut être la preuve de propriété. Une application antérieure à la preuve de propriété est notamment décrite dans le 35 document de M.Dwyer et J.Hatcliff Slicing software for model construction. In Partial Evaluation and Semantic-Based Program Manipulation (PEPM), pages 105 à 108, 1999. La technique que nous retenons est basée sur lefait que les propriétés à prouver peuvent être traduites en automates. Une solution est d'intégrer la propriété dans le modèle sous forme d'un automate supplémentaire qui contraint le modèle initial et de choisir comme critère de slicing toutes les transitions de cet automate. Cela permet notamment de ne garder dans le résultat que les parties du modèle initial utiles pour prouver la propriété. Une autre application possible concerne les modèles paramétrés pour lesquels on veut déterminer certains paramètres inconnus en fonction de propriétés à vérifier. Il est alors possible d'intégrer la propriété à vérifier sous forme d'automate supplémentaire qui contraint le modèle initial et cela permet de ne garder dans le résultat que les parties utiles pour déterminer les paramètres inconnus. Le critère de slicing est dans ce cas le même que pour la preuve, c'est l'ensemble des transitions de l'automate qui représente la propriété. Un autre exemple d'application peut être le test de conformité, un type de test de conformité étant notamment décrit dans le document de M.Bozga, JC Fernandez et L.Ghirvu Using static analysis to improve automatic test generation. Software Tools for Technology Transfer (STTT), pages 142-152, 2003. L'objectif de test peut être vu comme une propriété à tester et une solution possible est alors identique aux deux exemples d'applications précédents. La propriété à tester est intégrée au modèle sous la forme d'un automate supplémentaire qui la représente et ses transitions constituent le critère de slicing. Un quatrième exemple d'application est la gestion des évolutions pour un modèle, ces évolutions représentant les évolutions du système correspondant, par exemple dans une ligne de produits. Dans ce cadre, si la partie qui évolue est représentable sous la forme d'un sous-ensemble du système, cela permet de déterminer un sous-ensemble minimal d'automates du modèle incluant toutes les évolutions possibles a priori, les autres automates du modèle étant considérés comme stables, c'est-à-dire non sujets à évolutions. Une solution possible est de calculer quelle est la partie utile, notamment pour les phases de vérification ou de validation d'un produit, du sous-ensemble stable du système lors de l'intégration d'évolutions à venir. On applique à cet effet le procédé de slicing à la partie stable du modèle, en prenant comme critère toutes les transitions de cette partie stable du modèle qui ont une communication, en entrée ou en sortie, avec la partie qui peut faire l'objet d'une évolution. Les figures 6a et 6b illustrent un exemple d'application. Cette figure représente un système M dans lequel la sortie est la moitié de la valeur absolue de l'entrée du système. Par la suite, on note x - y une transition des figures 6a et 6b, la transition allant de l'état x à l'état y. La figure 6a représente un automate, ayant un état initial a, qui est l'interface du système avec un environnement et communique avec celui-ci par un canal ext. La figure 6b représente un automate, ayant un état initial f, qui est le noyau du système. L'automate de la figure 6a communique avec l'automate de la figure 6b par des canaux pos, neg. L'automate de la figure 6a reçoit une donnée transmise par l'interface, fait un calcul et retourne le résultat à l'interface. Si le critère de slicing est la transition i -> f, alors il est réduit à une transition de l'automate noyau, de la figure 6b, qui est celle qui va de l'état i vers l'état f, et donc qui retourne la valeur y par le canal neg à l'automate interface, de la figure 6a. L'analyse des dépendances dans le modèle, à l'aide des modules CD, DD et COM, donne notamment : - i -~ f est une transition données-dépendante de g - i ; i -~ f est aussi une transition communication-dépendante de d --* e ; d - e est une transition à son tour contrôle-dépendante et données-dépendante de b -~ d ; - b - d est une transition données-dépendante de a ù> b. Les transitions non citées ci-dessus ne sont pas atteignables depuis le critère via une séquence de dépendances, c'est-à-dire qu'il n'existe aucune séquence de dépendances (ne comportant pas plusieurs dépendances de communication consécutives) depuis une de ces transitions vers une transition du critère. Ces transitions sont représentées en traits pointillés sur les figures 6a et 6b et ne sont donc pas incluses dans le résultat M' qui est le modèle réduit. Il est à noter que dans M', g n'est plus atteignable depuis l'état initial f. La procédure de rétablissement de l'atteignabilité du module Slicing , sur cet exemple, consiste soit à changer l'état source de la transition g - i pour qu'il devienne f, soit à ajouter une transition vide de f à g. L'atteignabilité de l'état a depuis l'état e peut être rétablie de manière analogue. L'exemple illustré par les figures 6a et 6b montre notamment que des fonctionnalités orthogonales de la spécification sont distinguées clairement par le procédé de slicing complet. Cela peut permettre en particulier d'appliquer les différentes méthodes de vérification ou de validation envisagées, pour la preuve ou le test par exemple, en évitant au maximum l'explosion combinatoire dans les calculs. En effet, la plupart des données inutiles sont éliminées en amont par le slicing . En outre de façon 1 o générale, le slicing est beaucoup moins coûteux en temps de calcul, avec une complexité polynomiale, que les procédés de vérification ou de validation où la complexité est en général exponentielle. ANNEXE DESCRIPTIVE DES FIGURES 2 A 4 15 La référence 23, figure 2 correspond à l'étape suivante : Pour chaque tr dans ComD[trl, M], telle que viaCom[tr] et viaCom[trI] sont faux : insertion de tr dans worklist et dans Mi', et positionnement de viaCom[tr] à vrai. La référence 39, fiqure 3 correspond à l'étape suivante : Pour tout état s et 20 toute transition conditionnelle trc : Calcul des CD [tr, mi] en fonction des P[s, trc]. La référence 321, fiqure 3 correspond à l'étape suivante : Pour tout état s source d'un élément de conds[Mi] : si tous les éléments tr de conds[Mi] ayant s pour source sont tels que P[cible(trl), tr] contient autant d'éléments que tr a 25 de successeurs, alors : Pour chaque trc dans conds[Mi] : Mise à jour de P[cible(trl), trc] à partir de P[s,trc} ; Et insertion des successeurs de tri dans worklist. La référence 33, fiqure 3 correspond à l'étape suivante : Pour chaque trc dans conds[Mi] : Mise à jour de P[cible(trl), trc] ; Et insertion de trs dans 30 worklist. La référence 421, fiqure 4 décrit l'étape de Mise à jour de newlnfo pour tri, à partir de RD[trp], Kill[trp], et Gen[trp], pour tout prédécesseur trp de tri. 35 REVENDICATIONS 1. Procédé de réduction paramétrée d'un modèle M (2), le modèle M étant l'union de modèles Mi d'automates communicants, et comportant un ensemble T de transitions tr, l'ensemble T étant l'union d'ensembles Ti qui sont des restrictions de l'ensemble T aux modèles Mi, caractérisé en ce que le modèle M est transformé par un mécanisme d'analyse statique en une structure de données sous forme de tableaux d'ensembles de transitions CD[M], DD[M] et ComD[M], pour chaque transition tr les ensembles CD[tr, M], DD[tr, M] et ComD[tr, M] contenant respectivement les transitions qui impactent une transition tr par une relation de dépendance de contrôle (5), une relation de dépendance de données (6) et une relation de dépendance de communication (7), un sous-ensemble CRIT du modèle M étant défini, Crit étant l'ensemble des transitions qui appartient au sous-ensemble CRIT, un sous-ensemble Ti' étant la restriction de l'ensemble Crit à un sous-système Mi, chaque ensemble Ti' contenant pour chaque sous-système Mi toutes les transitions tr qui ont un impact sur les transitions de l'ensemble Crit selon l'une au moins des relations de dépendance précédentes (5, 6, 7), la restriction Mi' de chaque sous-système Mi étant déduite de chaque ensemble Ti', le modèle réduit M' (3) étant composé de l'ensemble des restrictions Mi'. 2. Procédé selon la revendication 1, caractérisé en ce qu'il comporte : une étape préliminaire (20) dans laquelle on calcule pour chaque transition tr de l'ensemble Crit les trois ensembles CD[tr, M], DD[tr, M] et ComD[tr, M], ces ensembles contenant respectivement les transitions qui impactent ladite transition tr par une dépendance de contrôle (5), une dépendance de données (6) et une dépendance de communication (7) ; une étape (20') de création d'un ensemble de travail (worklist) formé de l'union des sous-ensemble Ti' associée à deux fonctions booléennes viaCom[tr] et done[tr] où pour chaque transition tr, done[tr] est vrai si le traitement de la transition est terminé et viaCom[tr] est vrai si le traitement de la transition tr a été exécuté seulement via une dépendance de communication (7), viaCom[tr] et done[tr] étant initialisés à l'état faux pour toute transition, une transition tr n'étant traitée que si done[tr] est à l'état faux ;- un processus en boucle (11) formé de trois étapes (21, 22, 23), le processus étant terminé lorsque la liste de travail est vide, où ; dans la première étape (21), on extrait une transition tri de la liste de travail ; dans une deuxième étape (22), chaque transition tr des ensembles CD[trl, M] ou DD[trl, M] est insérée dans la liste de travail, puis si viaCom[tr] est faux et si tr appartient au sous-ensemble Ti, tr est ajouté au sous-ensemble Ti', puis viaCom[tr] est positionné à faux et done[tr] est positionné à vrai ; dans une troisième étape (23) chaque transition tr de l'ensemble ComD[tr], telle que viaCom[tr] et viaCom[trl] sont faux, est insérée dans la liste de travail, la transition tr appartenant à un sous-ensemble Ti, elle est ajoutée au sous-ensemble Ti', puis viaCom[tr] est positionné à vrai et l'élément tri est retiré de la liste 15 de travail. en fin de processus (21, 22, 23) chaque sous-ensemble Ti' contenant, pour chaque sous-système Mi appartenant au modèle M, toutes les transitions qui ont un impact sur les transitions de l'ensemble CRIT. 20 3. Procédé selon l'une quelconque des revendications précédentes, caractérisé en ce qu'un ensemble CD[tr, M] est obtenu selon un processus comportant : une étape d'initialisation (30), dans laquelle pour chaque sous-système Mi on construit un ensemble de transitions conditionnelles trc 25 conds[Mi], puis les ensembles CD[tr, Mi] sont initialisés à l'ensemble vide pour toutes transactions tr de Mi, et pour chaque état s de Mi et chaque transition conditionnelle trc dans conds[Mi] on définit un ensemble P[s, trc] qui est l'ensemble des chemins maximaux dans Mi qui commence par la transition trc et contiennent s, puis un ensemble 30 de travail comportant les transitions conditionnelles est créé ; - un processus en boucle formé de deux étapes (31, 32) où : dans une première étape (31), on extrait (311) de la liste de travail une transition tri ; dans une deuxième étape (32), on effectue (320) un test de 35 jointure sur l'élément tri extrait, si tri est à la jointure de plusieurschemins on effectue une mise à jour (321) de l'ensemble P[cible(trl), trc] et une mise à jour de la liste de travail, P[cible(trl), trc] étant l'ensemble des chemins maximaux qui partent de trc et passent par l'état cible de tri, de façon à ce que, si plusieurs transitions ont cible(tr) pour état cible, pour chaque état s tel qu'au moins une transition conditionnelle a s pour état source : -si toutes les transitions conditionnelles tr qui ont s pour état source sont telles que P[cible(trl), tr] et succs[tr, Mi] ont le même nombre d'éléments, P[cible(trl), tr] et succs[tr, Mi] étant respectivement l'ensemble des chemins maximaux qui partent de tr et passent par l'état cible tri et l'ensemble des successeurs de tr ; - alors pour toute transition conditionnelle trc appartenant à conds[Mi] différente de tri, si l'ensemble P[s, trc] contient des éléments que P[cible(trl), trc] ne contient pas, ces éléments sont ajoutés à l'ensemble P[cible(trl), trc] et tous les successeurs de tri sont ajoutés à l'ensemble de travail ; à la fin de cette étape (32) un test (322) étant effectué sur le nombre de successeurs de la transition tri, si le test (322) indique que tri a plus d'un successeur le processus reprend au niveau de la première étape (31), si le test (322) indique que tri à un seul successeur, trs, on met à jour (33) l'ensemble P[cible(trs), trc] à partir de P[cible(trl), trc] : pour toutes les transitions conditionnelles trc de conds[Mi], si l'ensemble P[cible(trl), trc] contient des éléments que P[cible(trs), trc] ne contient pas, ces éléments sont ajoutés à l'ensemble P[cible(trs), trc] et trs est ajouté à l'ensemble de travail ; la transition tri étant retirée de la liste de travail, le processus se terminant par une dernière étape (39) lorsque la liste de travail devient vide, dans cette dernière étape 39, pour tout état s de Mi et pour toute transition trc appartenant à conds[Mi], si P[s, trc], ensemble des chemins maximaux qui partent de trc et qui contiennent s : - contient le même nombre d'éléments que succs[trc, Mi] ; et s'il existe une transition trc' de conds[Mi] qui a le même état source que trc et telle que P[s, trc'] ait moins d'éléments que succs[trc', Mi] ;alors il existe un chemin depuis trc' qui crée une dépendance de contrôle de trc sur toutes les transitions tr dont l'état source est s on ajoute alors trc à l'ensemble CD[tr, Mi] en construction pour toutes ces transitions tr, l'ensemble CD[tr, M] étant l'union des ensemble CD[tr, Mi] ainsi obtenus pour tous les Mi. 4. Procédé selon l'une quelconque des revendications précédentes, caractérisé en ce qu'un ensemble DD[tr, M] est obtenu selon un processus comportant : - une étape d'initialisation (40) dans laquelle on définit, pour chaque sous-système Mi, deux tableaux Def et Ref d'ensembles de variables, indicés par les éléments de Ti, on définit trois tableaux Gen, Kilt et RD d'ensembles de définitions, une définition étant un couple (tr, v), formé d'une transition tr et d'une variable v, ces tableaux étant indicés par les éléments de Ti, et on définit deux ensembles de travail, un ensemble newinfo qui est un ensemble de définitions et un ensemble worklist qui est un ensemble de transitions, pour chaque transition tr de Ti, on initialise : Def[tr] par l'ensemble des variables, soit mises à jour par l'entrée de tr si elle existe, soit mises à jour par une affectation de tr ; Ref[tr] par l'ensemble des variables qui sont soit transmises par une sortie de tr à l'extérieur de l'automate qui contient tr, soit présentes dans la garde de tr, soit utilisées dans un terme qui est affecté à une variable, et tel que le résultat ne soit pas l'identité sur cette variable ; RD[tr] et DD[tr] par l'ensemble vide ; Gen[tr] par l'ensemble des couples (tr, v) où v appartient à Def[tr] ; Kill[tr] par l'ensemble des couples (trk, v) où trk est une transition quelconque de Ti différente de tr et où v appartient à Def[tr] ; Worklist par l'ensemble Ti. - un processus en boucle comportant deux étapes (41, 42) : - dans une première étape (41) on extrait (411) une transition tri de l'ensemble worklist que l'on nomme tri ; - dans une étape suivante (42) l'ensemble newinfo étant initialisé à vide, pour toute transition trp prédécesseur de tri on ajoute (421) à l'ensemble newinfo tous les éléments de RD[trp] sauf ceux qui appartiennent aussi à Kill[trp], et on ajoute à newinfo les élémentsde gen[trp], puis on réalise un test (422) sur l'ensemble newinfo , Si newinfo contient l'ensemble RD[trl] strictement alors on ajoute (423) ces éléments à RD[trl], puis on ajoute (424) les successeurs trs de tri à l'ensemble worklist et on retire tri de l'ensemble worklist , le processus se rebouclant sur la première étape (41) ; lorsque l'ensemble worklist devient vide, le processus se terminant par la dernière étape (49) dans laquelle, pour chaque transition tr de Ti, et pour chaque élément (trk,v) de RD[tr] : - si la variable v est utilisée dans la garde de tr ; - ou si la variable v appartient à Ref[tr] mais n'est pas affectée par l'entrée de la transition, si elle existe ; alors on ajoute trk à l'ensemble DD[tr, Mi] ainsi construit ; l'ensemble DD[tr, M] étant l'union des ensembles DD[tr, Mi] ainsi obtenus 15 pour tous les Mi. 5. Procédé selon l'une quelconque des revendications précédentes, caractérisé en ce qu'un ensemble ComD[tr, M] est obtenu selon un processus comportant : 20 - une étape préliminaire dans laquelle on définit deux tableaux d'ensembles de transitions emit et rcv indicés par les éléments d'un ensemble de canaux C qui est l'union des ensembles des canaux Ci des sous-systèmes Mi, l'ensemble ComD[tr, M] étant initialisé à vide ; - une première étape (51) de calcul des éléments de emit et de rcv de 25 telle façon que pour toute transition tr de T, où T est l'ensemble de toutes les transitions du modèle M : si tr appartient à Ti, Ti étant l'ensemble des transitions du i-ème automate du système ; si tr a une entrée, ou une sortie, et que cette entrée, ou cette sortie, 30 correspond à celle du canal c de Ci ; alors elle est ajoutée à l'ensemble emit[c] s'il s'agit de l'entrée ou à l'ensemble rcv[c] s'il s'agit de la sortie, emit[c] et rcv[c] étant respectivement les ensembles emit et rcv indicés par le canal c ;- une deuxième étape (52) de calcul des dépendances de communications dans le modèle, en se basant sur les informations de emit et rcv de telle façon que pour tout canal c de C et pour toute transition tre de emit[c], si l'ensemble Ti contient tre, alors pour toute transition trr de rcv[c] : - si l'ensemble Tj contient trr ; et si i est différent de j ; - on ajoute tre à ComD[trr, M] et on ajoute trr à ComD[tre, M] ; le calcul des ensembles ComD[tr, M] étant alors achevé.10