Le project SPECTRE a développé la boîte à outils CADP (CAESAR/ALDEBARAN Development Package) pour la conception et la mise au point de protocoles et de systèmes distribués. Construite autour du langage LOTOS (norme ISO 8807), cette boîte à outils offre des fonctionnalités de simulation, génération de code, vérification partielle et exhaustive, qui permettent de détecter au plus tôt les erreurs potentielles dans la conception de systèmes complexes, afin d'en accroître la fiabilité et à d'en diminuer les coûts de développement. Depuis 1993, la boite à outils fait l'objet d'une coopération internationale dans le cadre de deux projets successifs euro-canadiens, EUCALYPTUS-1 et EUCALYPTUS-2.
La boite a outils CADP a été diffusée à plus de 125 sites dans le monde entier et a été utilisée sur de nombreux exemples pratiques. Parmi ses applications les plus récentes, on peut mentionner: l'analyse du protocole BRP utilisé par Philips dans l'un de ses produits audiovisuels (INRIA), l'étude d'algorithmes distribués d'élection sur un réseau en anneau (INRIA), l'analyse de configurations ferroviaires (SICS, Suède), la caractérisation d'une erreur dans le protocole TCP (GMD-FOKUS, Allemagne), l'étude des interactions entre services téléphoniques (CWI, Pays-Bas), ainsi que la mise en défaut du protocole de sécurité Equicrypt basé sur le principe des ``tiers de confiance'' et destiné à contrôler l'accès à des services multimédia (Université de Liège, Belgique).
En particulier, dans le cadre de l'action VASY du GIE Bull/INRIA DYADE, la boîte à outils CADP/EUCALYPTUS est utilisée pour la vérification d'architectures multiprocesseurs développées par Bull. Elle a notamment permis de prouver la correction de l'arbitre de bus de l'architecture PowerScale mise en {\oe}uvre dans les stations de travails et serveurs Escala de Bull. Les travaux actuels portent sur le protocole de cohérence de caches de la future architecture multiprocesseurs devant équiper les machines haut de gamme Bull.
Back to the VASY Home Page