Ce travail porte sur la verification formelle de programmes paralleles. Parmi les methodes habituellement utilisees, nous nous interessons aux methodes basees sur la construction d'un modele du programme a verifier; la verification proprement dite s'effectue sur ce modele. Cette approche est limitee par l'explosion de la taille du modele, des que le programme traite est de complexite realiste. Notre but est l'etude et la mise en oeuvre de techniques permettant d'effectuer la verification malgre cette explosion. Les techniques que nous presentons sont liees par une caracteristique commune : l'utilisation de methodes symboliques de representation du modele. Nous etudions en premier lieu des techniques de reduction de modeles. Ces reductions s'operent par rapport a des relations d'equivalence basees sur la notion de bisimulation. Nous etudions en particulier un algorithme de minimisation de modele (\em pendant ) sa generation(Generation de Modele Minimal). Dans une seconde partie, nous nous interessons a deux techniques symboliques de representation de modeles. Il s'agit d'une part de Graphes de Decision Binaires, qui permettent la manipulation efficace de formules booleennes, et d'autre part de systemes d'inequations lineaires, connus sous le nom de polyedres convexes, pour la manipulation de variables entieres. L'utilisation de ces techniques permet de representer et manipuler des modeles de taille souvent prohibitive pour des methodes enumeratives classiques. Nous presentons la mise en oeuvre de methodes de comparaison et reduction de modeles aves les Graphes de Decision Binaires, avec en particulier l'algorithme de Generation de Modele Minimal. L'application de l'outil correspondant a plusieurs exemples de programmes lotos a permis de montrer l'interet, mais aussi les limites de l'utilisation de cette representation symbolique. Enfin, nous presentons une methode d'analyse statique de protocoles, basee sur l'utilisation des polyedres convexes. Cette analyse permet le calcul d'approximations superieures d'invariants du programme et de verifier la veracite de proprietes definies en termes de variables du programme.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00005100 |
| Date | 29 November 1994 |
| Creators | Kerbrat, Alain |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | French |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.002 seconds