en fr Parallel and distributed high-level colored Petri net model checking Model checking parallèle et réparti de réseaux de Petri colorés de haut-niveau : application à la vérification automatique de programmes Ada concurrReportar como inadecuado




en fr Parallel and distributed high-level colored Petri net model checking Model checking parallèle et réparti de réseaux de Petri colorés de haut-niveau : application à la vérification automatique de programmes Ada concurr - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

1 CEDRIC - Centre d-Etude et De Recherche en Informatique du Cnam 2 LIP6 - Laboratoire d-Informatique de Paris 6

Abstract : This thesis enters in the frame of the automatic verification of concurrent software based on an intermediary formal language : high-level colored Petri nets. We particularly endeavor to tackle the combinatorial explosion phenomenon induced by exhaustive exploration of all possible inter leavings of a system. We focus on taking advantage of the amount of memory and computing resources provided by a local network of workstations working cooperatively. For more efficiency, distribution of the system accessibility graph is based upon a structural analysis of the model. We also aim at preserving in this distributed environment the other techniques that try to limit the combinatorial explosion. We especially relax constraints on the graph exploration consistency. These approaches have then been validated and evaluated with our distributed and multithreaded model checker.

Résumé : Cette thèse s-inscrit dans le cadre de la vérification automatique de programmes concurrents basée sur un modèle formel intermédiaire: les réseaux de Petri colorés de haut-niveau. Nous nous attachons à combattre le phénomène d-explosion combinatoire lié à l-exploration explicite de l-ensemble des entrelacements possibles du système. Pour cela, nous nous proposons de tirer profit de la quantité de mémoire et de la puissance de calcul offerte par un réseau local de machines travaillant de manière coopérative. Par le biais d-une analyse structurelle, nous cherchons à répartir efficacement le graphe d-accessibilité du système. Nous nous attachons ensuite à conserver l-efficacité des techniques visant à limiter l-explosion combinatoire dans cet environnement réparti en relâchant notamment les contraintes de cohérence sur l-exploration du graphe. Nous avons alors validé ces approches à l-aide d-un vérifieur réparti et multithreadé dans lequel nous avons implémenté nos algorithmes.

Mots-clés : Model checking Répartition du processus de vérification Parallélisme Concurrence Réseaux de Petri Vérification de programmes concurrents





Autor: Christophe Pajault -

Fuente: https://hal.archives-ouvertes.fr/



DESCARGAR PDF




Documentos relacionados