PAJAULT Christophe
Direction de recherche : Jean-François PRADAT-PEYRE
Model Checking parallèle et réparti de réseaux de Petri colorés de haut-niveau
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.
Soutenance : 23/06/2008
Membres du jury :
Didier Buchs,
Gaétan Hains,
Franco Gasperoni,
Claude Girault,
Claude Kaiser,
Denis Poitrenaud
Dir. de thèse: Jean-François Pradat-Peyre
Publications 2008
-
2008
- Ch. Pajault : “Model Checking parallèle et réparti de réseaux de Petri colorés de haut-niveau”, soutenance de thèse, soutenance 23/06/2008, direction de recherche Pradat-peyre, Jean-François (2008)
- Ch. Pajault, J.‑F. Pradat‑Peyre, P. Rousseau : “Adapting Petri Nets Reductions to Promela Specifications”, Formal Techniques for Networked and Distributed Systems - FORTE 2008, 28th IFIP WG 6.1 International Conference, vol. 5048, Lecture Notes in Computer Science, Tokyo, Japan, pp. 84-98, (Springer-Verlag) (2008)
- C. KAISER, Ch. Pajault, J.‑F. Pradat‑Peyre : “Concurrent Program Metrics Drawn by Quasar”, Ada-Europe 2008, 13th Ada-Europe International Conference on Reliable Software Technologies, vol. 5026, Lecture Notes in Computer Science, Venice, Italy, pp. 101-114, (Springer-Verlag) (2008)