Garavel-Mateescu-Serwe-13

Génération et manipulation d'espaces d'états distribués avec CADP: expériences sur Grid'5000

Hubert Garavel, Radu Mateescu, and Wendelin Serwe

Actes de la 21ème Conférence en Parallélisme, Architecture et Système COMPAS'13 (Grenoble, France), January 2013

Résumé:

La vérification distribuée utilise les ressources d'un ensemble de machines pour accélérer et surtout pour accéder à des quantités de mémoire au delà de ce qui est possible avec une seule machine. Dans cet article, nous présentons les outils de vérification distribuée fournis par la boîte à outils CADP, en mettant l'accent sur les améliorations récentes des outils pour l'exploration à la volée de systèmes de transitions étiquetées partitionnés. Nous faisons aussi état des résultats d'expériences avec ces outils sur Grid'5000 utilisant jusqu'à 512 processus répartis.

18 pages
PDF

PostScript


Slides of W. Serwe's lecture at COMPAS'13
PDF