Brevet FR2771880A1 — publié le 19990604

PROCÉDÉ DE VÉRIFICATION DU FONCTIONNEMENT D'UN SYSTÈME La présente invention concerne le domaine de la vérification de systèmes. Les systèmes auxquels peut s'appliquer l'invention peuvent être de nature très diverse. Ils incluent notamment les logiciels informatiques séquentiels ou parallèles, les protocoles de communication, les systèmes de controle-commande, les systèmes répartis, les composants électroniques, etc. En règle générale, l'invention est applicable à tout système physique dont le fonctionnement peut se modéliser sous forme d'auto::ates communicants. On entend par modèle une abstraction du système permettant d'en paramétrer le fonctionnement. Dans le cas présent, c'est la traduction sous forme d'automates du système. Celle-ci doit bien sûr conserver le maxime de propriétés du système, tout en permettant une flexibilité vis-à-vis des méthodes de vérification employées. On entend par automate une représentation paramétrique d'une partie du système, formée d'états et de La vérification au sens de la présente invention consiste à démontrer que des propriétés du système tel que représenté par des automates sont vraies ou fausses, en exhibant un chemin ou en prouvant qu'un tel chemin ne peut pas exister, un chemin étant une succession (bien entendu possible) d'états globaux du modèle. Le chemin donne la suite ordonnée de chaque état de chaque élément du modèle. Dans le cas présent, ce sera la suite ordonnée d'états de chaque automate composant le modèle. Il faut noter que la vérification se fait en règle générale sur un modèle et non sur le système lui-même. Elle diffère en cela du test qui est plus directement lié au produit fini. Le test consiste à faire fonctionner le système réel (par exemple exécuter le logiciel) afin d'en étudier le comportement, en tentant de couvrir au maximum son fonctionnement. De nombreux ateliers de vérification permettent toutefois de générer automatiquement le système réel (le logiciel) à partir du modèle, ou d'en définir les spécifications. I1 existe un nombre assez important d'outils d'aide à la modélisation et à la vérification (voir par exemple A.A. Loureiro et al. : Fdt tools for protocol development , In FORTE'92, 1992). Dans le domaine de la vérification, trois types de méthodes sont le plus souvent employées 1. La simulation. La majorité des outils existants permettent de faire de la simulation. Elle correspond à parcourir les états du modèle les uns après les autres selon une stratégie plus ou moins sophistiquée, afin de rechercher des chemins pertinents. Cette méthode a l'avantage de pouvoir s'utiliser sur n'importe quel niveau d'abstraction du système (tant que cette abstraction possède la notion de chemin) et d'être très souple d'utilisation. Elle a deux inconvénients : elle se heurte à l'explosion combinatoire du nombre d'états du système (plus la recherche est profonde, plus le nombre de chemins est grand), et elle ne prouve rien (ne pas trouver de chemin en profondeur n ne prouve pas qu'il n'en existe pas en profondeur n+l). 2. Le model-checking (voir A. Kerbrat : Méthodes symboliques pour la vérification de processus communicants : étude et mise en oeuvre , Thèse de Doctorat, Université Joseph Fourier, Grenoble, 1994, ou K.L. McMillan : Symbolic Model Checking , Kluwer Academic Publishers, 1993). Les méthodes dites de modelchecking nécessitent une modélisation du système sous forme d'automates. Les automates de cette modélisation sont fusionnés en un unique automate dont chaque état correspond à un état global du modèle. Sur cet automate global, il est ensuite possible de vérifier des propriétés décrites en logique temporelle. L'avantage de cette méthode réside dans la richesse de la logique temporelle qui permet de spécifier un nombre très large de types de requêtes. Elle permet également de faire facilement de la simulation. Elle a cependant pour limitation de générer très rapidement un automate global de taille gigantesque qui en règle générale ne peut donc pas être construit, malgré un certain nombre de techniques réduisant la taille de cet automate (utilisation de techniques de codage de 1' automate global, fabrication d'un modèle de l'automate global aux propriétés plus faibles, etc.). 3. La preuve par théorèmes (voir J.-R. Abrial The B-book , Cambridge University Press, 1995, ou B. Chetali : Formal verification of concurrent programs: how to specify UNITY using the Larch t Prover , Technical report, INRIA, France, 1995) . Le modèle est ici constitué d'un ensemble de formules logiques qui en décrivent les propriétés de base. Une nouvelle propriété à vérifier étant donnée sous forme d'une formule logique, une preuve sera constItuée des étapes successives permettant d'obtenir cette nouvelle formule logique à partir des formules logiques du modèle et de règles d'inférence. Cette méthode a l'avantage de produire de vraies preuves formelles. Cependant, il n'existe pas à l'heure actuelle de bonnes stratégies d'inférence, et l'ordinateur est presque toujours réduit à ne résoudre que les étapes simples de la preuve et laisser les parties ardues au logicien humain. Dans le domaine des réseaux de Pétri, il est connu d'employer des méthodes d'optimisation faisant appel à la programmation linéaire pour effectuer de la vérification de systèmes. Cependant, la programmation linéaire n'est utilisée que sur des modèles très fortement contraints et donc non utilisables pour modéliser des systèmes réels (voir J. Esparza et al. : A polynomial-time algorithm to decide liveness of bounded free coince nets , Theoretical Computer Science, 102 :185-205, 1992), ou pour la génération de l'ensemble des invariants du modèle étudié (algorithme de Fourier-Motzkin e particulier), ensemble qui est construit sans discernement et qui devient rapidement de taille gigantesque. Plus récemment, une équipe a étudié l'utilisation de la programmation entière directement sur un modèle d'automates communicants (voir J.C. Corbett : Automated Formal Analysis Methods for Concurrent and Real-Time Software , PhD thesis, Department of Computer Science, University of Massachussets, USA, 1992). Mais l'utilisation de la programmation entière ne permet pas d'avoir d'algorithme efficace, et surtout ne permet pas de faire de preuve sur le modèle. Cette équipe a étudié de manière approfondie la puissance d'expressivité du système de requêtes, et en a déduit qu'elle était très proche de la logique temporelle. Une autre utilisation de la programmation linéaire dans le domaine de la vérification a été présentée par J.L. Lambert ( Présentation du projet validation de protocoles par programmation linéaire , Technical Report 27, Greyc, Université de Caen, 1994) . Cette approche ne fait pas intervenir de notion d'ordonnancement des messages, ce qui constitue une limitation quant aux conditions de fonctionnement du système qui peuvent être analysées. La présente invention a pour but d'enrichir les techniques de vérification, en proposant un procédé capable de prouver des propriétés du système étudié et dont la complexité ne croisse pas trop dramatiquement avec la taille du système. L'invention propose ainsi un procédé de vérification du fonctionnement d'un système modélisé par un système d'automates synchronisés par un ensemble de messages, comprenant les opérations suivantes - on décompose le système en un nombre N de soussystèmes numérotés de n=l à n=N - on fournit des paramètres décrivant chaque soussystème n (1#n#N) sous forme d'un automate respectif composé d'un ensemble E n d'états du sous-système n, avec un ensemble A n de transitions an@ entre paires d'états de l'ensemble En, chaque transition an de l'ensemble An étant associée à un sous-ensemble Mnj de l'ensemble des messages de synchronisation de façon à traduire le fait que chaque message du sous-ensemble Mnj survient lorsque le sous-système décrit change d'état conformément à la transition - on construit un système d'équations linéaires comprenant, pour 1#t#T et 1#n#N, d'une par des équations de flot de la forme et de la forme et d'autre part des équations de synchronisation de la forme où T désigne un nombre d'étapes successives du index j tels que la transition anj de l'ensemble An provienne de l'état eni de l'ensemble En' cni désigne l'ensemble des index j tels que la transition a? de l'ensemble An conduise à l'état en de l'ensemble En Mn désigne la réunion des sous-ensembles de messages respectivement associés aux transitions de l'ensemble An 3k désigne l'ensemble des index j tels qu'un message mk de l'ensemble Mn appartienne au sous-ensemble Mnj associé à la transition aj de l'ensemble An, la variable eni(t) (p#t#T) est une inconnue du système linéaire associée à l'état e n de l'ensemble E n et à l'étape t, la variable anj(t) (1#t#T) est une inconnue du système linéaire associée à la transition a de l'ensemble A n et à l'étape t, la variable mk (t) (lSt - on définit une propriété du système à vérifier, sous la forme de contraintes linéaires supplémentaires imposées aux inconnues du système linéaire - on applique au système linéaire soumis aux contraintes supplémentaires une méthode de résolution par programmation linéaire ; et - on analyse le résultat de la programmation linéaire pour déterminer si ladite propriété est vérifiée par le système. Ce procédé possède peu de points communs avec les trois méthodes antérieures commentées ci-dessus. Comme le model-checking , ii part d'une modélisation sous forme d'automates communicants, mais la s'arrête la comparaison. Le système de requêtes est du même ordre d'expressivité que la logique temporelle, bien qu'il soit plus proche de la notion de chemin que celle-ci : dans le cas présent, les requêtes sont typiquement basées sur des questions d'accessibilité d'états et de transitions, et d'envois ou de réception de messages. Une différence fondamentale avec e model-checking est que le procédé opère directement sur les automates de la modélisation sans passer par un automate global produit de tous les automates du modèle. D'autre part, les preuves que donne la programmation linéaire correspondent à des sommes d'équations permettant d'arriver à une équation trivialement fausse. Elles n'ont donc pas de rapport avec la preuve par théorèmes. Le procédé permet également de fournir des chemins validant une requête. Mais ce chemin est construit d'un bloc, sans parcours des états comme le ferait la simulation ou le model-checking. La solution proposée par la programmation linéaire n'est pas forcément un chemin à valeurs entières. Il convient donc de construire un modèle d'automates qui réduise au maximum le nombre de solutions non entières et qui permette, lorsqu'il en apparaît, de les interpréter et les éliminer, en introduisant ~ des contraintes linéaires supplémentaires pertinentes. D'autres particularités et avantages de la présente invention apparaîtront dans la description c- après d'exemples de réalisation non limitatifs, e référence aux dessins annexés, dans lesquels - la figure 1 est un schéma d'un exemple simple ce système auquel peut s'appliquer la présente invention - les figures 2 à 5 sont des diagrammes d'automates représentant des éléments du système de la figure 1 - les figures 6 et 7 sont des variantes de l'automate de la figure 5 ; et - les figures 8 à 11 sont des diagrammes montrant des chemins que le procédé permet de mettre en évidence dans le système d'automates. L'utilisation d'automates est courante dans le domaine de la vérification. Ils ont l'avantage d'être à la fois expressifs quant à la traduction du fonctionnement du système et faciles à appréhender et à manipuler par l'utilisateur. Le type d'automate utilisé par le procédé est assez classique ; l'invention réside essentiellement dans l'exploitation faite de cette modélisation par automates. Tous les éléments du système sont décrits sous la forme d'automates. Ces éléments, ou sous-systèmes, peuvent être des dispositifs appartenant au système, dont les automates représentent les états de fonctionnement. Ils peuvent également être de nature logicielle instruction ou commande échangée, données, canaux de transmission (files d'attente, piles...). Le système étudié étant décomposé en N soussystèmes, chacun de ces sous-systèmes n (lin Ces paramètres comprennent - le nombre I (n) d'états de l'automate sn ; on note E n = {eni , 1#i#I (n)} l'ensemble des I (n) états de l'automate Sn - le nombre J(n) de transitions de l'automate sn ; on note An = {anj, 1#j#J(n)} l'ensemble des J(n) transitions de l'automate sn ; pour chaque transition anj : l'identification de l'état eni d'où provient cette transition, et de l'état en auquel conduit cette transition. E-. d'autres termes, n la transition an fait passer le sous-système représenté par l'automate sn de l'état eni à l'état eni'. Ces paramètres permettent de déterminer deux ensembles Bni et Cni pour chaque état eni de l'ensemble En (1#i#I(n)) L'ensemble Bn est l'ensemble des index j tels que 1#j#J(n) et que la transition a? provienne de i i l'état de départ en. L'ensemble Cn est l'ensemble des index j tels que 1#j#J(n) et que la transition ag conduise à l'état d'arrivée en. Il est fait appel à un ordinateur pour la mise en oeuvre des calculs recuis par le procédé selon l'invention. Typiquement, cet ordinateur sera équipé d'une interface graphique permettant à l'utilisateur de fournir simplement les paramètres énumérés ci-dessus, définissant la structure des automates, en dessinant des noeuds représentant les transitions anj. La formation des ensembles Bni et Cni peut alors avoir lieu au fur et à mesure de l'introduction des états et transitions. A partir de ces ensembles et d'un nombre entier T fourni par l'utilisateur, l'ordinateur construit équations de flot. Le nombre T représente un nombre d'étapes successives de fonctionnement du système, sur lesquelles ce fonctionnement fait l'objet de la vérification. Les expressions de ces équations de flot sont, pour 1#t#T, 1#n#N et 1#i#I(n) Dans ces équations de flot (1f) et (2f), les variables eni(t) et anj(t) sont en principe à valeur binaire (0 ou 1). Quand eni(t)=1 (0#t#T), le sous-système n décrit par l'automate sn est dans l'état eni à l'issue de l'étape t et au début de l'étape t+l ; sinon, e (t)=0. Quand n n (1#t#T), le sous-système n décrit par l'automate Sn change d'état conformément à la transition an lors de l'étape t ; sinon, anj(t)=0. Le système d'automates S = {sn, 1S n Sn lorsque ceux-ci effectuent des transitions des ensembles An @ les messages de synchronisation mk accompagnent donc les transitions a;, de sorte que leur apparition peut se modéliser à l'aide des automates Sn. Ceci consiste, pour l'utilisateur, à associer chaque transition an de l'ensemble A n des transitions d'un automate sn à un sous-ensemble Mnj de l'ensemble M des messages de synchronisation. Cette association signifie que chaque message du sous-ensemble M survient lorsque n le sous-système décrit par l'automate 3n change d'état conformément à la transition anj. Lorsqu'une transition anj d'un automate sn est franchie, tout autre automate sn' ayant une ou plusieurs transitions an'J telles que accomplit l'une de ces transitions an'j'. Cette association est aisée à définir lorsqu'une interface graphique de l'ordinateur met à disposition de l'utilisateur une représentation graphique des états et transitions de l'automate : il suffit d'étiqueter chaque arc représentant une transition avec le ou les messages mk qui l'accompagnent. L'ordinateur est alors en mesure de définir les sous-ensembles Mnj pertinents. Il définit en outre, pour chaque automate Sn la réunion M des sousensembles de messages Mj respectivement associés aux transitions de l'ensemble An, soit On note (n) le nombre de messages de l'ensemble Mn. Il définit enfin, pour chaque message mk de l'ensemble M l'ensemble Dnk des index j tels que 1#j#J(n) et que le message mk appartienne au sous-ensemble Mnj associé à la transition anj, soit Certaines transitions an peuvent n'être accompagnées par aucun message de l'ensemble M (M = O). Le plus souvent, ces transitions auront des états de départ et d'arrivée identiques, ce qui traduit le fait que le sous-système en question ne change pas d'état en l'absence de messages. Dans la suite, on supposera qu'il existe une telle transition, dite arc #, pour chacun des états de chaque automate, et on notera tn l'ensemble des index des I (n) arcs # relatifs à l'automate Sn Mais on observera que cette supposition ne correspond qu'à un cas particulier auquel l'invention n'est pas limitée. A partir des ensembles Dnk définis par les relations de synchronisation, l'ordinateur construit équations de synchronisation, dont les expressions sont, pour 1#t#T, 1#n#N et mk#Mn : où mk(t) est une variable en principe binaire (0 ou 1). Quand mk (t) =l, le message mk survient pendant l'étape t sinon, mk(t)=0. Les équations de flot et de synchronisation (If), (2f) et (3s) forment un système linéaire dont les variables ni (t), a (t) et mk (t) constituent les inconnues. Conformément à l'invention, on cherche à résoudre ce système linéaire par une méthode de programmation linéaire, pour vérifier des propriétés du système définies sous la forme de contraintes linéaires supplémentaires imposées aux inconnues de ce système linéaire. Dans cette résolution, on fait l'hypothèse que les inconnues el (t), anj(t), mk(t) sont à valeurs positives ou nulles, mais non nécessairement entières. Les méthodes de résolution par programmation linéaire sont très classiques dans le domaine de l'optimisation combinatoire. Elles sont largement utilisées dans l'industrie grâce à leur efficacité et à l'étendue de leur champ d'application (voir par exemple Williams : Model Building in Mathematical Programming, Wiley, 3 édition, 1993 ; Chvatal : Linear Programmig g , Editions Freeman, 1983 ; ou encore R. Saigal : Linear Programming : A Modern Integrated Analysis , Editions Kluwer, 1996). Actuellement, des logiciels, tels que ceux commercialisés sous les appellations CPLEX et OSL, peuvent traiter en un temps raisonnable des systèmes de plusieurs millions de contraintes et dizaines de millions de variables. La complexité des algorithmes existants, qu'ils soient de type simplexe ou par points intérieurs, se situe entre le linéaire et le quadratique en la taille du problème (c'est-à-dire qu'un problème deux fois plus grand prendra entre deux et quatre fois plus de temps pour être résolu) . Mais sachant qu'en pratique, il est possible d'utiliser de nombreuses astuces d'optimisation, des gains considérables peuvent être obtenus sur ces temps de calcul. La programmation linéaire regroupe les méthodes permettant de trouver une solution positive assujettie à un ensemble de contraintes linéaires, et qui maximise un critère défini par une équation linéaire donnée. Voici une manière classique d'exprimer ce genre de problème : on cherche Un vecteur colonne x de taille p tel que où A est une matrice à m lignes et p colonnes, c un vecteur ligne de taille p, et b un vecteur colonne de taille m. Il est possible de modifier ce problème en y intégrant des inéquations, en enlevant certaines contraintes de positivité sur x, etc. Mais la linéarité de l'ensemble des équations doit être conservée, à la fois pour pouvoir utiliser un algorithme efficace et pour permettre d'interpréter les résultats. Les contraintes d'intégrité (cela correspond à faire de la programmation entière) sont à bannir pour les mêmes raisons. Pour comprendre la notion de preuve de programmation linéaire, le problème est plutôt formulé comme suit. On cherche toujours un vecteur x de taille p, ma s tel que Ce problème (5) semble plus simple puisqu'on ne cherche qu'à satisfaire l'ensemble des contraintes, sans optimiser en outre un critère linéaire. Mais il est en fait de même difficulté que le problème (4). Ce problème (5) possède alors la propriété suivante, dite lemme de Farkas : le système A.x = b, x > 0 n'admet pas de solution si et seulement si le système dual y.A > 0, y.b Si on suppose que le système de contraintes A est la traduction des automates décrits ci-dessus et d'une requête d'accessibilité à vérifier, le vecteur x étant composé des inconnues ei(t) aj(t) et mk(t) le lemme de n n Farkas assure que : (i) soit il existe un chemin validant la requête, c'est-à-dire un vecteur colonne x de taille p solution du problème direct, (ii) soit il y a une preuve que ce chemin n'existe pas, ctest-à-dire un vecteur ligne y de taille m solution du problème dual. L'algorithme de programmation linéaire exécuté par l'ordinateur va donc trouver ce x, ou s'il n'existe pas, le y correspondant. Les contraintes linéaires supplémentaires sont définies par l'utilisateur en fonction de la propriété qu'il cherche à vérifier. En général, on prévoit des contraintes linéaires pour fixer une configuration initiale du système d'automates, c'est-à-dire les valeurs des variables eni(0) pour iSnAN et l Pn désigne une partie non vide de l'intervalle [1,I(n)], qui imposent à l'état initial de l'automate d'être dans une certaine partie de l'ensemble En. Les contraintes supplémentaires comprennent d'autres relations linéaires à satisfaire par les inconnues du système linéaire, se rapportant à l'état final (à t=T) de certains automates, à l'accomplissement de certaines transitions et/ou à ltémiss on de certains messages de l'ensemble M. Dans certains cas, des contraintes supplémentaires pourront en outre être définies en introduisant dans la modélisation un ou plusieurs automates spécifiques appelés automates observateurs. Dans le cadre de l'invention, les contraintes supplémentaires peuvent encore inclure un critère linéaire à optimiser, c'est-à-dire que la programmation linéaire peut aussi être utilisée selon la formulation (4) cidessus. Ceci permet d'identifier le meilleur chemin au sens du critère optimisé. Des exemples de tels critères sont dont la maximisation permet d'identifier le chemin qui implique le moins de changements d'états ; la sommation pourrait également porter sur seulement une partie des automates Sn ; dont a minimisation permet d'identifier le chemin qui nécessite le moins d'envois de messages de synchronisation ; la sommation pourrait également porter sur seulement une partie de l'ensemble M des messages mk dont la minimisation permet d'identifier le chemin pour lequel un automate Sn reste le moins longtemps dans l'un de ses états en... Dans les critères indiqués ci-dessus, les sommes pourraient encore être pondérées. Dans certains cas, la programmation linéaire peut produire une solution non entière, au moins une des composantes du vecteur x étant différente de 0 et de 1. Dans un tel cas, on ne peut pas conclure immédiatement sur la propriété examinée : soit il n'existe aucune solution entière et la propriété n'est pas vérifiée, soit la solution non entière cache une solution entière et la propriété est vérifiée. Plusieurs approches sont possibles lorsqu'une solution non entière se présente. On peut ainsi affiner la requête en ajoutant ou en modifiant des contraintes linéaires avant de réitérer l'application de la méthode de résolution par programmation linéaire. L'utilisateur est en cela guidé par la structure de la solution non entière. Par exemple, si le chemin solution comporte la composante mk (t) =p/q, p et q étant des entiers tels que O Des contraintes du même genre peuvent être introduites si l'utilisateur détecte que, selon la solution non entière, certains automates se retrouvent dans un état suspect avec une variable d'état en (t) fractionnaire, ou suivent une transition suspecte avec une variable de transition ani (t) fractionnaire... Fréquemment, cette façon de faire permettra d'obtenir une solution entière concluante. Dans certains cas, on pourra également réduire le nombre T d'étapes de calcul, afin d'éliminer des solutions non entières dans lesquelles des transitions fractionnaires répétées sur plusieurs étapes sont susceptibles de constituer une transition complète. Pour s'affranchir de solutions non entières, on peut encore recourir à des critères linéaires à optimiser. Si la première résolution du système linéaire pour vérifier une propriété donne lieu à une solution non entière, on peut rechercher d'autres solutions du même système qui optimisent divers critères linéaires. Certaines de ces autres solutions peuvent être entières et donc prouver la propriété recherchée. Sinon les différents essais peuvent aider à diagnostiquer que la propriété n'est pas vérifiée. Une solution non entière peut encore apparaître lorsque certains défauts de modélisation sont présents dans le système d'automates synchronisés. La structure de la solution non entière peut aider l'utilisateur à détecter ces défauts et à y remédier par une modification appropriée des paramètres décrivant le système. On va maintenant Illustrer le procédé à l'aide d'un exemple représenté sur les dessins annexés. Cet exemple est délibérément très simplifié pour illustrer aussi clairement que possible les opérations effectuées conformément à l'invention. On comprendra que la puissance des métho téléphone X vers le téléphone Y, et à un canal de transmission du téléphone Y vers le téléphone X. On suppose, pour simplifier, cue seul le téléphone X est habilité à demander l'établissement d'une connexion avec le téléphone Y, alors que la déconnexion peut être demandée par l'un ou l'autre des deux téléphones. Dans ces conditions, l'ensemble M des messages de synchronisation se compose de six messages (K=6) - rn émis par le téléphone X pour demander l'établissement d'une connexion avec U ; - in2 émis par le téléphone X pour demander la déconnexion - m3 émis par le téléphone Y pour demander la déconnexion ; - m4 reçu par le téléphone Y pour provoquer sa connexion avec X ; - m5 reçu par le téléphone Y pour provoquer sa déconnexion ; et - m6 reçu par le téléphone X pour provoquer sa déconnexion. Les automates synchronisés S1 et S2 relatifs aux téléphones X et Y sont représentés sur les figures 2 et 3. Ils comportent chacun deux états ( connecté et déconnecté ) et cinq transitions : I(l)=I(2)=2, J(1)=J(2)=5. Ces deux automates introduisent les équations suivantes dans le système linéaire à résoudre Equations de flot : (n=l ou 2) Equations de synchronisation Le canal de transmission du téléphone Y vers le téléphone X est simple : il fait uniquement transiter le message de déconnexion de Y vers X. Il est représenté par un automate 53 comportant deux états et quatre transitions (I(3)=2, J(3)=4), comme représenté sur la figure 4. Cet automate introduit les équations suivantes dans le système linéaire à résoudre Equations de flot Equations de synchronisation Pour le canal de transmission du téléphone X vers le téléphone Y, trois cas différents sont envisagés sur les figures 5, 6 et 7. On considère d'abord le cas de la figure 5, où le canal n'accepte de faire transiter des messages que par paquets de deux (par exemple pour des raisons d'efficacité de la transmission) . Après avoir reçu le paquet constitué par les deux messages ml et m2 (transition a4), le canal retransmet les deux messages correspondants m4 et m5 vers le téléphone Y (transition a42). On note que cette transmission est modélisée comme étant asynchrone puisque l'automate S4 est autorisé à rester dans l'état e42 selon un are # (transition a44). Pour modéliser une transmission synchrone, il suffirait de supprimer cette transition a44 de l'ensemble A4 des transitions de l'automate. L'automate S4 de la figure 5 comporte deux états et quatre transitions (I(4)=2, J(4)=4). Il introduit les équations suivantes dans le système linéaire à résoudre Equations de flot Equations de synchronisation Une première série de propriétés du système qu'on peut vérifier est le fait que chaque état de fonctionnement d'un sous-système n, représenté par un état de l'automate correspondant 5n peut être atteint à partir d'une configuration de départ donnée, et que chaque message de synchronisation de l'ensemble Mpeut survenir. La configuration de départ est par exemple : les deux téléphones déconnectés et aucun message en transit dans les canaux : ceci correspond aux contraintes linéaires supplémentaires suivantes pour 1#n#4 : en1(0)=1 et en2(0)=0. Pour vérifier si l'état e n d'un automate Sn peut être atteint, on impose la contrainte supplémentaire e n (T)=l en choisissant une valeur modérée du nombre T. Si la programmation linéaire fournit une solution, l'état en est accessible. Sinon, il n'est pas accessible en T étapes. Dans ce dernier cas, on peut augmenter la valeur du nombre T pour rechercher l'existence éventuelle d'une solution. Si on considère que le nombre T devient trop important sans qu'on trouve de solution, on peut diagnostiquer que la modélisation est incorrecte et y remédier, ou estimer que le système étudié ne fonctionne pas dans la mesure où l'un de ses états est inaccessible. Le système modélisé par les automates S1 à S4 des figures 2 à 5 ne vérifie pas cette propriété dès que l'état dont on examine l'accessibilité diffère de l'état initial : la programmation linéaire ne propose aucune solution. Ceci traduit le fait que le canal modélisé par l'automate S4 de la figure 5 est totalement bloquant puisque l'automate S1 ne peut jamais émettre les messages ml et m2 en même temps. Le même genre de vérification peut être effectué pour la possibilité de décrire une transition donnée ou d'émettre un message donné. Par exemple, dans le cas de l'émission du message m5 à partir de la configuration de départ ci-dessus, on ajoute la contrainte linéaire qui traduit le fait que le message m5 aura été émis une fois parmi les T étapes successives. Là encore, le système modélisé par les automates S1 à 54 des figures 2 à 5 ne vérifie pas cette propriété. Dans le cas de la figure 6, le canal du téléphone X vers le téléphone Y permet de faire transiter l'un ou l'autre des messages de connexion et de déconnexion (par exemple parce que c'est un canal à faible débit). L'automate S4 comporte alors deux états et six transitions (S(4)=2, J (4) =6). . Il introduit les équations suivantes dans le système linéaire à résoudre Equations de flot Equations de synchronisation Le système modélisé par les automates S1 à s4 des figures 2, 3, 4 et o vérifie la première série de propriétés évoquée ci-dessus. Dans une deuxième phase de vérification, on peut examiner des propriétés plus complexes que la simple accessibilité d'un état, d'une transition ou d'un message. On peut par exemple rechercher si tout message reçu par un téléphone correspond bien à celui qui a été envoyé par l'autre téléphone. Par exemple, pour tester que le message de demande de déconnexion par le téléphone X est toujours bien reçu par le téléphone Y, on peut examiner si la propriété inverse est vérifiée pour un certain chemin dans le modèle d'automates, en ajoutant les onze contraintes linéaires suivantes (téléphones connectés à t=0) (canaux vides à t=0) (X demande la déconnexion à la le étape) (aucune connexion redemandée) (Y reçoit une demande de connexion) La figure 8 montre un chemin formant une solution en 1=5 étapes du système linéaire soumis à ces onze contraintes supplémentaires, dans ie cas du système modélisé par les automates S1 à S4 des figures 2, 3, 4, et 6. Comme la propriété vérifiée révèle un fonctionnement anormal du système, on peut déduire de l'existence de cette solution procurée par la programmation linéaire que le système modélisé fonctionne mal. L'utilisateur peut interpréter ce mauvais fonctionnement : le canal de X vers Y modélisé sur la figure 6 est susceptible d'introduire des erreurs, de sorte qu'il paraît nécessaire de faire la distinction entre les messages pour éviter ce type de mauvais fonctionnement. La solution de la figure 8 n'est pas nécessairement fournie directement par la programmation linéaire. Le système linéaire soumis aux onze contraintes supplémentaires admet en effet des solutions non entières que la programmation linéaire est susceptible de produire dans un premier temps. Une telle solution non entière est illustrée par la figure 9. Si l'utilisateur obtient cette solution, il ne peut pas conclure immédiatement quant à la propriété examinée. Il peut par contre observer que les messages m3 et m4 semblent se dédoubler, et essayer de réduire le nombre T d'étapes de fonctionnement. Pour T=2, une nouvelle résolution le conduira alors à la solution entière de la figure 8. Dans le cas de la figure 7, le canal du téléphone X vers le téléphone Y permet de faire transiter l'un ou l'autre des messages de connexion et de déconnexion, en faisant la distinction entre ces deux essages. L'automate S4 comporte alors trois états et sept transitions (I (4) =3, J (4) =7). Il introduit les équations suivantes dans le système linéaire à résoudre Ouations de flot Equations de synchronisation Le système modélisé par les automates S1 à S4 des figures 2, 3, 4 et 7 vérifie la première série de propriétés évoquée ci-dessus. La figure 10 illustre par exemple un chemin, correspondant à une solution trouvée par la programmation linéaire, qui prouve que le système est bien capable de générer le message m5 en 1=5 étapes depuis la configuration où les deux téléphones sont déconnectés (contraintes supplémentaires : en1(0)=1, en2(0)=0 Le système modélisé par les automates S1 à S4 des figures 2, 3, 4 et 7 ne vérifie pas les propriétés qui ont révélé le mauvais fonctionnement du système modélisé par les automates S1 à S4 des figures 2, 3, 4 et 6 (en particulier, la programmation linéaire ne fournit aucune solution au système linéaire assorti des onze contraintes supplémentaires évoquées ci-dessus). Dans une troisième phase de vérification, on examine si le système peut se bloquer, c'est-à-dire si un canal peut avoir en transit un message que le téléphone destinataire est incapable de lire. Par exemple, pour déterminer si le canal de X vers Y est susceptible de contenir un message de demande de déconnexion alors que le téléphone Y est déconnecté, on utilise les contraintes supplémentaires (téléphones déconnectés à t=0) (canaux vides à t=0) (téléphone Y déconnecté à t=T) (message de déconnexion en transit à t=T) La programmation linéaire montre que le système linéaire soumis à ces contraintes supplémentaires admet une solution entière, représentée sur la figure Il. Le système modélisé par les automates S1 54 des figures 2, 3, 4 et 7 risque donc de se bloquer. En analysant la solution de la figure 11, l'utilisateur peut se rendre compte de ce que le problème survient lorsque les deux téléphones demandent simultanément la déconnexion. Pour s'affranchir de ce genre de problème, il faut avoir recours à un protocole comportant des messages d'acquittement, ce qui implique de mosafier chacun des automates de la modélisation et d'ajouter des messages dans l'ensemble M. Le procédé selon l'invention pourra à son tour être appliqué à cette nouvelle modélIsation afin d'en examiner les propriétés. REVENDICATIONS 1. Procédé de vérification du fonctionnement d'un système modélisé par un système (S) d'automates synchronisés par un ensemble de messages (M), comprenant les opérations suivantes - on décompose le système en un nombre N de soussystèmes numérotés de n=l à n=N ; - on fournit des paramètres décrivant chaque soussystème n (l - on construit un système d'équations linéaires (1f, 2f, 3s) comprenant, pour l et de la forme et d'autre part des équations de synchronisation de la forme où T désigne un nombre d'étapes successives du fonctionnement du système, B n désigne l'ensemble des index j tels que la transition anj de l'ensemble An provienne de l'état eni de l'ensemble En' Cni désigne l'ensemble des index j tels que la transition anj de l'ensemble A n conduise à l'état e n de l'ensemble Eni M n désigne la réunion des sous-ensembles de messages Mnj respectivement associés aux transitions de l'ensemble An Dnk désigne l'ensemble des index j tels qu'un message mk de l'ensemble Mn appartienne au sous-ensemble Mnj associé à la transition a? de l'ensemble An, la variable en (t) (0StST) est une inconnue du système linéaire associée à l'état e n de l'ensemble E n et à l'étape t, la variable anj(5) (1#t#T) est une inconnue du système linéaire associée à la transition anj de l'ensemble An et à l'étape t, la variable mk (t) (1#t#T) est une inconnue du système linéaire associée au message mk de l'ensemble (M) des messages de synchronisation et à l'étape t - on définit une propriété du système à vérifier, sous la forme de contraintes linéaires supplémentaires imposées aux inconnues du système linéaire - on applique au système linéaire soumis aux contraintes supplémentaires une méthode de résolution par programmation linéaire ; et - on analyse le résultat de la programmation linéaire pour déterminer si ladite propriété est vérifiée par le système. 2. Procédé selon la revendication 1, dans lequel on détermine que ladite propriété est vérifiée lorsque la programmation linéaire révèle que le système d'équations linéaires soumis aux contraintes supplémentaires a une solution dans laquelle chacune des variables (el (t), a (t), mk (t)) a soit la valeur 0 soit la valeur 1, et on détermine que ladite propriété n'est pas vérifiée lorsque la programmation linéaire révèle que le système d'équations linéaires soumis aux contraintes supplémentaires n'a pas de solution. 3. Procédé selon la revendication 1 ou 2, dans lequel, lorsque la programmation linéaire révèle que le système d'équations linéaires soumis aux contraintes supplémentaires a une solution dans laquelle l'une au moins des variables (eni(t), anj(t), mk(t)) a une valeur non entière, on modifie les contraintes supplémentaires, puis on réitère l'application de la méthode de résolution par programmation linéaire. 4. Procédé selon la revendication 1, 2 ou 3, dans lequel les contraintes linéaires supplémentaires comprennent une combinaison d'inconnues du système linéaire qui définit un critère linéaire à optimiser par la méthode de résolution par programmation linéaire.