Source: https://raweb.inria.fr/rapportsactivite/RA2001/vasy/resul_VASY-2001-5-1_mn.html
Timestamp: 2019-05-25 07:22:41+00:00

Document:
Développement de l'outil BISIMULATOR
Développement de l'outil PROJECTOR 2.0
Développement des outils DISTRIBUTOR 2.0 et BCG_MERGE 2.0
Autres développements d'outils
En 2001, nos travaux sur la vérification ont porté sur l'extension et l'amélioration d'outils existants, ainsi que sur le développement de nouveaux outils visant à faciliter l'utilisation des techniques formelles en milieu industriel.
Participants : Hubert Garavel, Frédéric Perret.
des systèmes de transitions ``ordinaires'', tels que ceux produits à partir de descriptions LOTOS ;
des systèmes de transitions ``probabilistes'' dont chaque transition peut être étiquetée, soit par une action a ``ordinaire'', soit par une probabilité p [0, 1], soit par un couple (a, p) ;
des systèmes de transitions ``stochastiques'' dont chaque transition peut être étiquetée, soit par une action a ``ordinaire'', soit par un paramètre réel qui détermine une loi de distribution exponentielle donnée par prob(x > t) = e- t, soit par un couple (a, ).
De par l'existence de ces différents types de transitions, les modèles acceptés par BCG_MIN sont suffisamment généraux pour couvrir de nombreux modèles probabilistes et stochastiques .
BCG_MIN fait partie de la boîte à outils CADP et ses performances sont reconnues : ainsi, il est cité dans [GvdP00] comme ``the best implementation of the standard algorithm for the branching bisimulation''. Concrètement, BCG_MIN permet de minimiser efficacement des graphes de grande taille que d'autres outils tels qu'ALDÉBARAN et FC2MIN ne parviennent pas à traiter par manque de mémoire. Par ailleurs, l'utilisation du format très compact BCG entraîne des gains à la fois en place disque et en rapidité.
En 2001, les travaux relatifs à BCG_MIN ont porté sur plusieurs points :
Nous avons entrepris d'optimiser BCG_MIN afin de traiter des graphes de taille plus importante. Le plus grand graphe minimisé par BCG_MIN en 2000 comportait 6 millions d'états et 11 millions de transitions, mais des limitations en mémoire empêchaient d'aller au-delà.
Après un examen attentif des algorithmes et des structures de données utilisés dans BCG_MIN, nous avons mis en oeuvre diverses optimisations destinées à réduire la consommation en mémoire.
Ainsi, la taille mémoire allouée pour une transition est passée de 20 à 16 octets. De même, la taille mémoire allouée pour un état est passée de 36 à 20 octets dans le cas des systèmes de transitions ordinaires, et de 44 à 28 octets dans le cas des systèmes de transitions probabilistes et stochastiques.
Ces progrès ont permis d'augmenter la taille des graphes traités par BCG_MIN. C'est ainsi que la nouvelle version de BCG_MIN a permis de minimiser un graphe de 8 millions d'états et 43 millions de transitions fourni par N. Zuanon dans le cadre de FORMALFAME (voir § 5.3.1 et 6.2).
La base de tests développée pour BCG_MIN en 1999 et 2000 a été améliorée afin de permettre le passage automatique des tests de non-régression à chaque modification du code de BCG_MIN.
Nous avons utilisé BCG_MIN pour la vérification fonctionnelle et l'évaluation de performances du protocole d'arbitrage du bus SCSI-2. Un article a été écrit et soumis à une conférence internationale.
L'utilisation de relations de bisimulation (équivalence forte, équivalence de branchement, équivalence observationnelle, etc.) pour la vérification comporte deux aspects complémentaires : la minimisation d'un graphe -- telle qu'effectuée notamment par l'outil BCG_MIN (voir § 5.1.1) -- et la comparaison de deux graphes selon une certaine relation d'équivalence.
C'est ce second aspect que nous avons abordé en 2001, en développant un nouvel outil appelé BISIMULATOR. Cet outil prend en entrée deux graphes à comparer, l'un représenté implicitement au moyen de l'environnement OPEN/CÆSAR [8], l'autre représenté explicitement sous forme de fichier BCG. BISIMULATOR permet de déterminer, soit si ces deux graphes sont équivalents au sens de la bisimulation forte, soit si l'un d'eux est inclus dans l'autre au sens du préordre associé à la bisimulation forte.
BISIMULATOR fonctionne à la volée, c'est-à-dire qu'il explore dynamiquement, au fur et à mesure des besoins, les parties utiles du graphe représenté implicitement, sans nécessiter de construire préalablement la totalité de ce graphe, ce qui pourrait s'avérer prohibitif.
De plus, l'utilisation des environnements génériques BCG et OPEN/CÆSAR rend BISIMULATOR totalement indépendant du langage source utilisé pour décrire les deux graphes à comparer. Ceci constitue un progrès significatif par rapport à des outils plus anciens -- tels qu'ALDÉBARAN et FC2IMPLICIT -- qui implémentent également certains algorithmes de comparaison à la volée, mais de manière limitée, puisqu'ils imposent au graphe implicite d'être fourni sous la forme d'un produit d'automates communicants, alors que BISIMULATOR peut s'appliquer directement à un programme écrit dans un langage de haut niveau (par exemple, LOTOS).
L'approche utilisée dans BISIMULATOR consiste à formuler le problème de la comparaison de deux graphes en termes d'un système d'équations booléennes. Comparer les graphes à la volée revient alors à effectuer la résolution locale du système booléen, c'est-à-dire à calculer la valeur de vérité de la variable représentant l'équivalence des états initiaux des deux graphes.
BISIMULATOR comporte environ 2 500 lignes de code C et il réutilise les fonctionnalités de résolution de systèmes booléens avec production de diagnostics développées en 1999-2000 pour l'outil EVALUATOR 3.0 [10,12]. Ces fonctionnalités ont été regroupées dans une bibliothèque générique appelée CÆSAR_SOLVE (1 500 lignes de code C) qui est utilisée conjointement par EVALUATOR 3.0 et par BISIMULATOR.
Les expérimentations que nous avons effectuées sur des graphes allant jusqu'à 10 000 états montrent une vitesse d'exécution de BISIMULATOR environ 25 fois supérieure à celle des algorithmes de comparaison à la volée pour la bisimulation forte implémentés dans l'outil ALDÉBARAN. Nous n'avons pas pu poursuivre plus avant les expérimentations car, au-delà de 10 000 états, les temps d'exécution des algorithmes à la volée deviennent prohibitifs.
Une fonctionnalité importante de BISIMULATOR consiste en la production de diagnostics expliquant pourquoi deux graphes sont équivalents ou inclus l'un dans l'autre (exemples) ou pourquoi ils ne le sont pas (contre-exemples). En pratique, ces diagnostics ont diverses utilités :
Les exemples produits par BISIMULATOR pour l'inclusion au sens du préordre de la bisimulation forte servent à améliorer les fonctionnalités du simulateur graphique OCIS, en lui permettant de relire interactivement les parties de graphes (traces d'exécution, scénarios, diagnostics, etc.) produites par d'autres outils de CADP tels que EXECUTOR, EXHIBITOR, EVALUATOR 3.0, etc.
Les contre-exemples produits par BISIMULATOR permettent à l'utilisateur de comprendre pourquoi deux graphes ne sont pas équivalents ou inclus : ces contre-exemples sont des graphes acycliques rassemblant toutes les séquences de transitions qui, exécutées simultanément dans les deux graphes, mènent à des états non équivalents. De ce fait, les contre-exemples de BISIMULATOR sont (beaucoup) plus compacts que ceux d'ALDÉBARAN, qui se limitent à un ensemble de séquences d'exécution construites séparément.
Nous envisageons d'étendre BISIMULATOR pour traiter le cas des bisimulations faibles (équivalence observationnelle, équivalence de branchement, etc.), ce que permet l'approche basée sur les systèmes d'équations booléennes.
La boîte à outils CADP comporte actuellement deux évaluateurs de logique temporelle : XTL [9], qui permet de vérifier de façon énumérative des formules temporelles comportant des données et EVALUATOR 3.0 [10,12], qui permet de vérifier à la volée des formules du -calcul régulier d'alternance 1 sans données.
Ces deux logiciels sont stables et robustes. Ils ont été utilisés avec succès pour valider 16 applications critiques, notamment en milieu industriel (par exemple, par BULL et ERICSSON). En 2001, ils ont été déposés à l'Agence pour la Protection des Programmes (APP).
Toutefois, dans un souci d'ergonomie, il serait souhaitable de proposer aux utilisateurs de CADP un seul outil d'évaluation de logique temporelle qui réunirait l'ensemble des fonctionnalités actuellement fournies par XTL et EVALUATOR 3.0 de manière séparée. C'est pourquoi, nous avons entrepris, en 2000, un travail d'unification d'XTL et d'EVALUATOR 3.0 qui devrait, à terme, aboutir à un outil de vérification unique, appelé EVALUATOR 4.0. A notre connaissance, il n'existe à l'heure actuelle aucun outil de vérification réunissant toutes ces fonctionnalités.
Cet outil permettra de vérifier à la volée des propriétés temporelles comportant des données. Le langage d'entrée d'EVALUATOR 4.0 sera basé sur des formules d'un -calcul régulier d'alternance 1 étendu avec des variables typées ; comme XTL, il offrira des primitives de manipulation des états et des transitions dans les formules logiques, permettant de définir des propriétés temporelles non-standard (comme par exemple le fait qu'un état possède une transition vers lui-même).
En 2001, nous avons poursuivi les travaux sur EVALUATOR 4.0 dans les directions suivantes :
Suite au retour d'utilisation d'EVALUATOR 3.0 par BULL dans le cadre de FORMALFAME (voir § 5.3.1 et 6.2), nous avons étendu le langage d'entrée d'EVALUATOR 4.0 avec de nouveaux opérateurs réguliers permettant d'exprimer la répétition bornée (entre n1 et n2 fois, où n1 et n2 sont des constantes entières) d'une séquence régulière de transitions. Combinés avec les modalités de possibilité et de nécessité, ces nouveaux opérateurs autorisent une description concise des propriétés du type ``chaque action d'émission sera suivie, après 15 transitions maximum, d'une action de réception''. Nous avons défini la sémantique de ces opérateurs en les traduisant vers les opérateurs de point fixe paramétrés déjà présents dans le langage d'entrée d'EVALUATOR 4.0.
Nous avons continué le développement de la ``partie avant'' d'EVALUATOR 4.0 qui effectue l'analyse syntaxique et sémantique du langage d'entrée (liaison des identificateurs, typage des expressions et des formules, résolution des surcharges), ainsi que diverses transformations sémantiques sur les formules temporelles. Développée à l'aide du générateur de compilateurs SYNTAX et du compilateur TRAIAN (voir § 4.2), la partie avant d'EVALUATOR 4.0 comporte désormais 15 000 lignes de code SYNTAX, LOTOS NT et C.
En 2001, nos efforts ont porté sur la traduction des formules temporelles en systèmes d'équations booléennes paramétrées par des variables typées. Nous traduisons d'abord ces formules vers des systèmes d'équations modales récursives ayant des variables propositionnelles en partie gauche et des formules PDL [FL79] en partie droite. Après avoir transformé ces systèmes afin que les parties droites des équations contiennent au plus un opérateur booléen ou modal, nous les traduisons finalement vers des systèmes d'équations modales récursives ayant des formules HML [HM85] en partie droite.
Enfin, nous avons poursuivi nos recherches théoriques afin d'optimiser l'évaluation à la volée des formules de logique temporelle dans le cas particulier où le système de transitions à vérifier est un graphe sans circuit. Ce cas particulier présente un intérêt pratique, notamment pour valider des séquences d'exécution finies (produites en laissant s'exécuter un système réel) à l'aide de formules de logique temporelle ; cette approche est utilisée dans le cadre de FORMALFAME pour vérifier la correction des traces de grande taille (comportant des dizaines ou des centaines de milliers de transitions) obtenues par test aléatoire de l'architecture multi-processeur FAME développée par BULL.
Nous avons établi que, dans le cas des graphes sans circuit, le -calcul modal d'alternance quelconque possède la même expressivité que son fragment d'alternance 1. Pour démontrer ce résultat, nous avons proposé une traduction du -calcul modal vers le -calcul gardé (formules dans lesquelles tout appel récursif d'une variable propositionnelle est précédé par une modalité), puis un algorithme d'évaluation basé sur une réduction sémantique des formules du -calcul gardé (équivalence des plus petits et plus grands points fixes) lorsqu'elles sont évaluées sur des graphes sans circuit.
Ce résultat permet de réduire fortement la complexité de la vérification : au lieu d'une complexité exponentielle comme dans le cas des graphes avec circuits, les formules de -calcul modal d'alternance quelconque peuvent être vérifiées avec une complexité linéaire en taille du graphe (nombre d'états et de transitions) et quadratique en taille de la formule (nombre d'opérateurs). En particulier, notre algorithme ne stocke en mémoire que les états visités, mais non les transitions. Ce travail a donné lieu à une publication [20].
Entre 1997 et 2000, nous avions conçu un langage appelé SVL (Script Verification Language), ainsi que le compilateur associé à ce langage, dans le but de simplifier et d'automatiser la mise en oeuvre des techniques de vérification compositionnelle et pour rendre celles-ci réellement utilisables dans un contexte industriel (et notamment par BULL, qui souhaitait les utiliser). En 2000, de nombreuses améliorations avaient été apportées au langage SVL et le compilateur avait été complètement réécrit.
Le compilateur SVL traduit chaque scénario de vérification en un shell script UNIX contenant la séquence de commandes (appels aux différents outils de vérification) correspondant à l'exécution de ce scénario. Les outils de vérification peuvent appartenir soit à CADP (ALDÉBARAN, CÆSAR, BCG, EXP.OPEN, OPEN/CÆSAR, PROJECTOR, etc.), soit à la boîte à outils FC2TOOLS développée dans l'ex-projet MEIJE (INRIA Sophia-Antipolis). Cette traduction est transparente pour l'utilisateur qui n'a plus à se soucier de la syntaxe d'appel propre à chaque outil. En outre, le compilateur SVL prend en charge la gestion des nombreux fichiers intermédiaires (abstractions, renommages, synchronisations, etc.) nécessaires à la vérification compositionnelle.
A l'origine, SVL a été conçu spécifiquement pour la vérification compositionnelle, en remplacement de l'outil DES2AUT [KM97]. En 2001, nous avons entrepris d'appliquer SVL dans un cadre beaucoup plus large que celui de la vérification compositionnelle, en l'utilisant pour simplifier les études de cas fournies dans la boîte à outils CADP comme exemples de démonstration. C'est ainsi que 19 études de cas (sur un total de 29) ont été réécrites en SVL. Ce faisant, nous avons pris conscience que SVL pouvait jouer le rôle d'un puissant langage de scripts dédié à la vérification, remplaçant avantageusement les Makefiles et shell scripts utilisés jusqu'alors, améliorant la lisibilité et supprimant un grand nombre de fichiers auxiliaires (désormais engendrés automatiquement par SVL).
Ces multiples expérimentations nous ont conduit à améliorer la définition du langage SVL :
De nouvelles instructions permettant la recherche des blocages et des bouclages infinis, ainsi que l'évaluation de formules de -calcul modal ont été intégrées au langage.
De multiples améliorations de la syntaxe ont été mises en oeuvre : de nouveaux symboles en notation infixée ont été introduits pour l'opérateur d'abstraction, d'autres opérateurs ont été renommés, et les règles de précédence, d'associativité et de portée des opérateurs unaires et binaires ont été ré-étudiées. Le nombre des modifications et le soin apporté à chacune d'elles ont conduit à un langage plus homogène, donc d'apprentissage et d'utilisation plus faciles.
Il est désormais possible, dans une description SVL, de créer et de manipuler explicitement des fichiers représentant des réseaux d'automates communicants au format EXP ou FC2. Auparavant, ces formats n'étaient que des formes intermédiaires produites et effacées automatiquement par SVL. Cette nouvelle fonctionnalité permet à présent d'appliquer plusieurs vérifications à la volée sur un même réseau d'automates communicants sans qu'il soit nécessaire de le regénérer à chaque vérification.
L'ergonomie du compilateur SVL 2.0 a également été améliorée sur de nombreux points :
La syntaxe d'appel du compilateur SVL en ligne de commande a été simplifiée. Les paramètres passés à SVL ont été classés en deux ensembles distincts (commandes et options) et certains d'entre eux ont été renommés pour plus de clarté.
Une nouvelle commande a été introduite, qui permet de visualiser le programme obtenu après la phase d'expansion syntaxique pendant laquelle certaines opérations complexes (dites meta-opérations) sont remplacées par des opérations plus simples.
Les conventions de nommage des fichiers temporaires ont été améliorées : au lieu de générer, pour ces fichiers, des noms sans signification, SVL leur donne désormais des noms qui suggèrent à l'utilisateur l'origine et le contenu de ces fichiers, tout en garantissant l'unicité des noms.
Durant l'exécution d'un script, SVL construit un fichier contenant la totalité des opérations effectuées (appels aux différents outils, résultats et messages produits par les outils, etc.) afin de fournir à l'utilisateur toutes informations utiles en cas d'échec de l'exécution, sans avoir à relancer SVL dans un mode de débogage.
La nouvelle version de SVL détecte et corrige dynamiquement certaines erreurs commises par l'utilisateur, ce qui peut éviter d'interrompre des vérifications parfois très longues. Ainsi, SVL peut modifier (avec avertissement) certains paramètres lorsque la vérification ne peut pas être effectuée avec les paramètres choisis par l'utilisateur. Il signale également certaines erreurs fréquentes, telles que l'inadéquation entre les étiquettes et le mode de filtrage lors des masquages et renommages d'étiquettes, ou l'utilisation d'interfaces trop restrictives lors de l'abstraction de processus communicants.
Des stratégies ``intelligentes'' ont été incorporées à SVL, pour lui permettre de résoudre divers problèmes comme le ferait un expert en vérification. Ainsi, si une minimisation par bisimulation avec ALDÉBARAN ou FC2 échoue, alors SVL essaie d'utiliser plutôt BCG_MIN si la relation d'équivalence choisie le permet. De même, si une minimisation pour une relation faible (par exemple, l'équivalence observationnelle) échoue, alors SVL tente d'effectuer d'abord une pré-minimisation avec une relation plus forte (équivalence de branchement ou équivalence forte) ayant plus de chances de réussir (car algorithmiquement moins coûteuse). En dernier recours, si toutes les tentatives ont échoué, SVL poursuit son exécution avec le système de transitions non réduit.
Ces multiples améliorations ont accru significativement la taille du compilateur SVL 2.0, qui est passée de 4 000 lignes de code (en 2000) à 6 300 lignes (soit 1 600 lignes de code SYNTAX et C, 2 900 lignes de code LOTOS NT et 1 800 lignes de shell script). Par ailleurs, la documentation du langage et du compilateur SVL a été mise à jour.
Distribué depuis juillet 2001, SVL 2.0 a été déjà utilisé par l'Université de Twente (Pays-Bas) pour la vérification compositionelle de systèmes stochastiques, ainsi que par les sociétés BULL et ERICSSON (Suède). Les premiers retours d'utilisation sont très positifs.
Enfin, les travaux consacrés à SVL ont donné lieu à une publication d'ensemble [17] et feront l'objet d'une démonstration publique [19] en 2002.
Participants : Hubert Garavel, Radu Mateescu, Gordon Pace.
Dans le prolongement direct du développement de SVL 2.0 (voir § 5.1.4), nous avons entrepris en 2001 des recherches pour améliorer les performances des techniques de vérification compositionnelle avec abstractions [GLS96,KM97] intégrées à la boîte à outils CADP.
Bien que ces techniques nous paraissent, dans leur principe, pertinentes pour lutter contre le problème de l'explosion d'états (voir § 2.2), leur implémentation dans l'outil PROJECTOR n'était pas optimale : des problèmes de lenteur et de consommation mémoire excessive pouvaient empêcher l'utilisation effective de la vérification compositionnelle.
Pour résoudre ces problèmes, nous avons entrepris de développer une nouvelle version de l'outil PROJECTOR (travail post-doctoral de G. Pace), en repartant uniquement des définitions théoriques [KM97] et sans aucunement considérer l'implémentation existante de PROJECTOR.
Bien que cette nouvelle version (550 lignes de code C) ne soit pas totalement achevée, les premières mesures de performances sont encourageantes puisque l'on obtient, sur certains exemples, des gains en rapidité pouvant atteindre un facteur 15.
Participants : Adrian Curic, Hubert Garavel, Christophe Joubert, Radu Mateescu, Gilles Stragier.
Nous étudions depuis 1999 l'utilisation de machines parallèles pour améliorer les performances des algorithmes de vérification énumérative.
Nos efforts se sont concentrés sur la parallélisation de l'algorithme de construction du graphe, qui constitue un goulot d'étranglement pour la vérification puisqu'il requiert un espace mémoire considérable pour stocker tous les états accessibles. La parallélisation de cet algorithme devrait permettre, en remplaçant la mémoire d'une seule machine par celle de dizaines ou de centaines de machines, de gagner plusieurs ordres de grandeur dans la complexité des graphes traités.
Nos travaux avaient abouti en 2000 à deux outils prototypes :
DISTRIBUTOR 1.0, qui répartit la construction d'un graphe sur N machines communiquant deux à deux au moyen de sockets. Chaque machine est chargée de construire une partie du graphe sous forme d'un fichier au format BCG, les états étant répartis entre les mémoires locales des machines au moyen d'une fonction de hachage déterminée statiquement.
BCG_MERGE 1.0, qui assemble les N parties de graphe construites sur chaque machine par DISTRIBUTOR afin d'obtenir un fichier BCG unique représentant le graphe complet.
Ces outils ont été expérimentés sur diverses architectures : stations de travail sous SOLARIS reliées par un réseau ETHERNET 100 Mbits et grappe de 12 PC sous LINUX interconnectés par un bus SCI. Les résultats obtenus sur des applications de grande taille (autour de 15 millions d'états) ont montré des accélérations importantes et un bon équilibrage de charge entre les machines. Ces résultats ont fait l'objet d'une publication [18].
En 2001, nous avons poursuivi nos travaux (dans le cadre des stages successifs d'A. Curic, de G. Stragier et de Ch. Joubert) afin d'augmenter les performances, la robustesse et l'ergonomie des outils et de permettre leur passage à l'échelle sur un nombre plus important de machines. Ces travaux ont abouti à un nouvel outil DISTRIBUTOR 2.0, entièrement réécrit (6 200 lignes de code C), qui apporte les améliorations suivantes :
Les communications entre processus ont été optimisées : utilisation de sockets non-bloquantes (plus rapides que les sockets bloquantes utilisées dans DISTRIBUTOR 1.0), réduction du nombre de connexions nécessaires à la transmission des paramètres aux machines distantes, gestion optimisée des tampons logiques de communication, etc. Par ailleurs, le code de DISTRIBUTOR 2.0 est plus modulaire, car les mécanismes de communication entre processus ont été clairement séparés de l'algorithme d'exploration proprement dit.
Dans son principe, l'outil DISTRIBUTOR est indépendant de tout langage de spécification particulier, puisqu'il s'appuie sur l'interface de programmation OPEN/CÆSAR [8] pour explorer le graphe à construire. Néanmoins, l'implémentation de DISTRIBUTOR 1.0 comportait certaines dépendances résiduelles par rapport au langage LOTOS, qui ont été supprimées de DISTRIBUTOR 2.0.
Une innovation importante de DISTRIBUTOR 2.0 consiste en l'introduction d'un processus auxiliaire (processus superviseur) qui s'exécute pendant toute la durée de la construction du graphe. Ce processus est notamment responsable du lancement des processus de génération répartis sur chacune des N machines et du lancement de l'outil BCG_MERGE 2.0 après terminaison de la génération distribuée.
DISTRIBUTOR 2.0 rassemble dans un fichier de configuration unique la totalité des paramètres nécessaires à la génération distribuée (nom des machines, répertoires de travail sur chaque machine, taille de la mémoire locale, taille des tampons de communication, etc.). Ce fichier de configuration permet de donner à ces paramètres des valeurs générales, valables pour la totalité des machines, valeurs pouvant ensuite être spécialisées pour certaines machines particulières. Cette approche est préférable à celle de DISTRIBUTOR 1.0 qui exigeait un fichier séparé pour chacune des machines, une solution fastidieuse et source d'erreurs lorsque le nombre de machines est élevé.
Le cas de la terminaison ``normale'' de la génération distribuée était déjà traité par DISTRIBUTOR 1.0 au moyen d'un algorithme de détection fonctionnant sur un anneau virtuel à jeton. DISTRIBUTOR 2.0 prend également en compte le cas de la terminaison ``anormale'' qui survient, soit lorsqu'une machine doit s'arrêter par suite d'un problème grave (pénurie de mémoire, par exemple), soit lorsque l'utilisateur décide d'interrompre prématurément la génération distribuée. Ceci a nécessité l'ajout, dans DISTRIBUTOR 2.0, d'un protocole spécial entre le processus superviseur et les processus répartis sur les N machines afin de permettre l'arrêt d'urgence, tout en laissant le système dans un état cohérent (fermeture des sockets et des fichiers BCG ouverts, terminaison des processus répartis, etc.).
DISTRIBUTOR 1.0 n'offrait pas à l'utilisateur la possibilité de suivre en temps-réel la progression de la génération distribuée. Pour remédier à cette lacune, DISTRIBUTOR 2.0 comporte une interface graphique (500 lignes de code TCL-TK) qui permet de visualiser en temps-réel diverses informations statistiques sur la construction du graphe : nombre d'états visités et explorés (sur chaque machine et globalement), nombre de transitions franchies (sur chaque machine et globalement), ensemble des étiquettes rencontrées, répartition des états entre les différentes machines, consommation mémoire, taux d'utilisation des processeurs, etc. Ces statistiques sont calculées localement sur chaque machine, puis transmises au processus superviseur qui les centralise et les affiche sur l'interface graphique.
Enfin, nous avons développé l'outil BCG_MERGE 2.0 (450 lignes de code C), qui constitue une refonte complète de BCG_MERGE 1.0 pour le rendre compatible avec la gestion des paramètres de configuration faite dans DISTRIBUTOR 2.0.
Les nouveaux outils DISTRIBUTOR 2.0 et BCG_MERGE 2.0 ont été expérimentés sur la grappe de 225 PC du projet APACHE. Les expériences ont porté sur diverses spécifications LOTOS (protocole du réseau HAVi, protocole d'arbitrage du bus SCSI-2, protocole d'élection sur des anneaux à jeton, etc.) traitées sur des configurations allant jusqu'à 70 machines. Les résultats observés confirment les résultats précédemment obtenus avec DISTRIBUTOR 1.0 et BCG_MERGE 1.0 sur des configurations plus réduites, à savoir une accélération importante et un bon équilibrage de charge entre les machines.
Participants : Hubert Garavel, Frédéric Lang, Stéphane Martin, Radu Mateescu, Bruno Ondet, Frédéric Perret.
En 2001, une part de nos travaux a été consacrée à l'intégration des résultats de recherche obtenus lors des dernières années au sein d'une version stable de CADP, appelée CADP 2001 ``Ottawa'' (voir § 8.1) :
Nous avons effectué un test systématique et rigoureux des différents outils de CADP afin de détecter les erreurs résiduelles.
Nous avons finalisé le portage de CADP vers le système d'exploitation WINDOWS et fait les changements nécessaires pour prendre en compte les versions récentes de WINDOWS et du logiciel CYGWIN de REDHAT.
Nous avons amélioré le simulateur OCIS sur divers points et mis à jour la documentation et l'aide en ligne pour cet outil.
Nous avons étendu le format EXP utilisé en entrée par les outils ALDÉBARAN, EXP.OPEN et EXP2FC2, puis modifié ces trois outils afin qu'ils interprètent ce format de manière identique.
Nous avons développé une extension des bibliothèques CÆSAR_HIDE et CÆSAR_RENAME de l'environnement OPEN/CÆSAR afin de prendre en compte les expressions régulières généralisées définies dans la norme POSIX.
Après la parution de CADP 2001, de nouvelles améliorations ont été effectuées :
Un nouvel outil appelé SEQ.OPEN a été développé afin de répondre aux besoins de BULL dans le cadre de FORMALFAME (voir § 6.2). SEQ.OPEN permet d'appliquer à un ensemble de traces d'exécution encodées dans le format SEQ les différents outils disponibles dans l'environnement OPEN/CÆSAR. Un avantage important de SEQ.OPEN réside dans le fait qu'il fonctionne sans charger en mémoire la trace d'exécution et peut, par conséquent, s'appliquer à des traces de très grande taille.
L'outil Bcg_Info a été étendu afin d'afficher des informations supplémentaires (facteur de branchement d'un graphe, liste des états de blocage, etc.)
L'outil Bcg_Io a été étendu pour produire le format DOT utilisé par les outils graphiques GRAPHVIZ développés par AT&T.
Enfin, nous avons établi une connexion directe entre CADP et l'atelier MUCRL développé par le CWI (Pays-Bas), afin de résoudre certaines difficultés pratiques rencontrées par la société ERICSSON (Suède) qui utilise conjointement les outils CADP et MUCRL. Cette connexion permet désormais à l'outil INSTANTIATOR du CWI de produire directement des graphes au format BCG.

References: § 5
 § 5
 § 5
 § 4
 § 5
 § 2
 § 8
 § 6