|
|
|
Ce rapport fait le point sur les travaux effectués dans le cadre du contrat BULL-INRIA FORMALFAME PLUS pendant la période allant du 23 mars 2004 au 1er octobre 2004.
| BULL | Jack Abily Sylvie Lesmanne (chef de projet) Solofo Ramangalahy (jusqu'au 31 mai 2004) Yehong Xing |
| INRIA / VASY | Damien Bergamini (ingénieur expert) Hubert Garavel (directeur de recherche) Radu Mateescu (chargé de recherche) |
L'équipe VASY a apporté son soutien à BULL sur divers problèmes ponctuels :
Réponses à des questions relatives à l'utilisation des outils CADP et à la modélisation en LOTOS.
Aide pour la paramétrisation de la spécification LOTOS de PRR. La spécification LOTOS du bloc PRR est désormais paramétrée ce qui permet de générer des traces pour les six instances possibles sans qu'il soit nécessaire de recompiler totalement la spécification. Auparavant, le numéro d'instance du bloc PRR figurait "en dur" dans le code LOTOS.
Fourniture de solutions de compatibilité permettant aux outils de CADP de fonctionner sur d'anciens systèmes Linux RedHat 7.3. La compatibilité avec RedHat 7.3 est particulièrement importante pour BULL car les outils certifiés de Cadence ne fonctionnent pas sur des versions plus récentes de Linux. L'équipe VASY a fourni plusieurs réponses successives (patches pour la librairie BCG, outil MCL_EXPAND compatible avec Linux RedHat 7.3, puis scripts de compatibilité pour la bibliothèque glibc 2.2.5 permettant aux outils CADP de fonctionner de manière transparente sous Linux RedHat 7.3). Ces solutions ont permis à BULL de mener à bien la campagne de couverture pour le B_SPS V1 sur Linux.
Ecriture d'un guide pour l'utilisation des nouvelles fonctions SAVE et RESTORE de l'API EXEC/CAESAR qui permettent de revenir à un état quelconque de la simulation.
Aide à la migration vers la bêta-version CADP 2003-i (juillet 2004) intégrant de nouveaux outils (CAESAR.BDD, EXP.OPEN 2.0 ...), notamment pour ce qui concerne la conversion des itérateurs sur les types LOTOS écrits manuellement en langage C.
Modification de INSTALLATOR afin que l'utilisateur puisse choisir entre rsh, ssh et krsh ce qui permet d'éviter les temps d'attente induits par la détection automatique du protocole (problème signalé par Jack Abily et Solofo Ramangalahy).
Mise à jour du fichier HISTORY détaillant tous les changements effectués dans la boîte à outils CADP (demande de Solofo Ramangalahy).
Ajout d'une fonctionalité dans CADP pour prévenir par e-mail l'utilisateur de l'expiration prochaine de ses licences CADP (par exemple, 30 jours avant l'expiration).
De nombreux changements ont été faits pour permettre la compatibilité avec les versions récentes de Linux (noyau 2.6) et des dernières versions des outils Unix disponibles sous Linux (tar, uncompress, uudecode, etc.) Ceci devrait permettre à BULL de migrer sans problème vers de nouvelles versions de Linux dès que les outils Cadence le permettront.
Parallèlement, la boîte à outils a été révisée pour accroître la portabilité du code en supprimant les aspects non compatibles avec la norme POSIX.
Le compilateur de types abstraits CAESAR.ADT a été enrichi afin de permettre la production automatique d'itérateurs pour les types structurés finis "complexes", tels que les paquets de données utilisés dans les protocoles de FAME. Dorénavant, l'utilisateur n'a plus à écrire ces itérateurs à la main en langage C, ce qui constitue un gain indéniable en temps et en fiabilité. Cette amélioration a nécessité une refonte complète du traitement des itérateurs dans CAESAR.ADT. De grands efforts ont été faits pour préserver une compatibilité ascendante, mais dans certains cas, une mise à jour du code LOTOS et/ou des itérateurs écrits à la main est nécessaire. De telles modifications ont été effectuées par BULL (après la migration vers CADP 2003-i) sur les spécifications LOTOS des blocs ILU et PRR, et n'ont pas soulevé de problème particulier.
Le traitement des "grands" réseaux de Petri (sujet abordé en 2003 dans l'étude de la spécification ILU) a été notablement amélioré par l'introduction de méthodes symboliques basées sur des diagrammes de décision binaires (BDDs, pour Binary Decision Diagrams). Un nouvel outil CAESAR.BDD a été ajouté à la boîte à outils CADP ; il permet de détecter les transitions "mortes" et les unités concurrentes d'un réseau de Petri sauf; cet outil utilise des BDDs. L'optimisation E7 implémentéee dans le compilateur CAESAR et permettant la suppression des transitions non accessibles du réseau de Petri engendré lors de la compilation a été totalement reécrite. La nouvelle version s'appuie sur le nouvel outil CAESAR.BDD et affiche de bien meilleures performances en temps, de telle sorte qu'il est désormais possible d'effectuer l'optimisation E7 de manière systématique : celle-ci est maintenant appliquée par défaut. L'utilisateur peut toutefois la supprimer s'il le désire grâce à l'option -e7 de CAESAR.
Pour la vérification compositionnelle, l'outil EXP.OPEN 2.0 a été intégré à CADP. Cette nouvelle version offre de nouvelles fonctionnalités et des performances très supérieures à l'ancienne.
Back to the VASY Home Page