Abstract FR:

Actuellement, le domaine de la verification est confronte au probleme de l'explosion combinatoire des systemes modelises. Les axes de recherche pour lutter contre ce probleme se portent a la fois sur la realisation d'algorithmes rapides, et sur la mise au point de techniques visant a contourner le delicat probleme de la taille de tels systemes. En ce qui concerne, les algorithmes rapides, nous presentons un algorithme de calcul de points fixes dont la complexite est lineaire. D'autre part, plusieurs approches comme par exemple la verification a la volee, ou les representations plus compactes a l'aide de diagrammes binaires de decisions, permettent d'attenuer le probleme de la taille des systemes modelises. Nous avons choisi d'explorer une nouvelle approche qui consiste a repartir le systeme sur plusieurs processeurs. Nous presentons donc egalement une etude sur la parallelisation de l'algorithme lineaire de calcul de points fixes. Pour chaque algorithme, sequentiel et parallele, et c'est un des aspects original de cette etude, nous avons effectue une importante phase d'experimentations. Cette analyse nous a permis de verifier tout d'abord que la complexite de l'implementation sequentielle etait bien conforme au modele theorique, et ensuite la pertinence de l'approche parallele.