Warning! The following job offer is no longer available.
Analyses statiques pour la réduction d'espace d'états en vérification énumérative
Vérification formelle - analyse statique
Le projet de Master 2 Recherche (ex-DEA) proposé s'effectuera à l'INRIA Rhône-Alpes au sein du projet VASY qui développe des outils logiciels pour la vérification de systèmes asynchrones. De tels systèmes couvrent un large domaine d'applications, allant du logiciel en passant par les protocoles de télécommunications aux systèmes et réseaux sur puce.
Le projet de Master porte sur l'utilisation d'analyses statiques pour la reduction de l'espace d'états d'un système asynchrone.
L'approche de vérification suivi par le projet VASY s'inscrit dans le cadre de la vérification énumérative, c'est-à-dire par exploration des états accessibles d'une spécification formelle du système. La limitation majeure de ces techniques étant l'explosion combinatoire de l'espace d'états, plusieurs techniques ont été proposées pour réduire le nombre d'états à explorer. Une technique consiste à insérer automatiquement des instructions de remise à zéro des variables dès que leur valeur n'est plus utilisée par la suite, ce qui peut être déterminé en analysant statiquement le flot de données. La remise à zéro peut réduire la taille de l'espace d'états de plusieurs ordres de grandeur [GS04].
Récemment, une généralisation de cette approche a été proposé dans le cadre de programmes impératifs concurrents [YG04]. L'idée est de calculer pour chaque variable X et chaque point du programme p une condition C telle que si au cours de l'exécution C est valide (au point p), alors X peut être remis à zéro. L'objectif du stage est l'étude de cette technique, appellée « analyse de variables partiellement mortes » dans le contexte des algèbres de processus et en connexion avec les outils de CADP développés par le projet VASY de l'INRIA Rhône-Alpes.
Ce projet de Master abordera donc les thèmes suivants :
En fonction de l'intérêt des résultats obtenus, ce projet pourra déboucher sur une thèse au sein du projet VASY.
| [GS04] | Hubert Garavel and Wendelin Serwe. State Space Reduction for Process Algebra Specifications. Dans "AMAST 2004", Lecture Notes in Compuer Science 3116, pages 164-180, juillet 2004. |
| [YG04] | Karen Yorav and Orna Grumberg. Static Analysis for State Space Reductions Preserving Temporal Logics. Dans "Formal Methods in System Design", 25(1), pages 67-96, juillet 2004. |
Pour plus d'informations concernant ce projet, contacter de préférence par courrier électronique, Wendelin.Serwe@inria.fr, téléphone : 04 76 61 53 52.