Micaela Mayero Homepage

stage_rdp_coq

Sujet de stage
Réseaux de Petri et preuves formelles

Encadrement : Micaela Mayero
Lieu :

LIPN, CNRS UMR 7030, équipe LCR

Université Paris13

99 avenue Jean-Baptiste Clément

93430 VILLETANEUSE

Contacts : Micaela.Mayero [@] lipn.univ-paris13.fr

Financement : oui
De nos jours, les systèmes à modéliser et à analyser sont de taille de plus en plus grande. Pour s’affranchir des problèmes inhérents à l’explosion du nombre d’états du réseaux de Petri, une spécification est souvent développée pas à pas (ce qui correspond à une démarche classique de développement de génie logiciel). Tout d’abord, un modèle abstrait est défini. Une fois que ses propriétés sont vérifiées, une étape de raffinement, qui introduit un niveau de détail supplémentaire, peut être effectuée et prouvée formellement.
Objectif du stage:
Trois types de raffinement ont été introduits par Lakos et Lewis, pour les réseaux de Petri de haut niveau : le raffinement de sous-réseau, le raffinement de noeud et le raffinement de type. Outre les avantage du raffinement pour la spécification de systèmes, ils permettent de faciliter la vérification de propriétés. En effet, d’une part certaines propriétés sont préservées par le raffinement, et d’autre part, l’analyse du modèle abstrait permet de guider celle du modèle concret, économisant ainsi du temps de calcul et de l’espace mémoire lors de la construction de graphes d’états. Jusqu’à présent, le processus de raffinement de réseaux était complètement manuel. La vérification des contraintes peut être assez complexe. Par conséquent, nous souhaitons prouver automatiquement qu’un réseau est effectivement un raffinement d’un autre réseau (abstrait). Pour cela, nous utilisons des techniques de preuve de théorémes, en particulier, l’assistant d’aide à la preuve Coq, développé à l’INRIA. Nous proposons donc une formalisation en Coq des définitions de raffinements ainsi que des réseaux auquels ils s’appliquent. Ceci a pour l’instant été développé pour les raffinements de sous-réseaux et de noeuds, et appliqué à quelques exemples.
Le but de ce stage est de généraliser la formalisation de raffinement de réseaux de Petri dans Coq. En particulier, il s’agira de proposer et de mettre en oeuvre des méthodes générales de spécification et d’automatisation de preuves. Une interface entre un outil tel que CPN-AMI et Coq pourra être faite.
Prérequis:
Le stagiaire ne devra pas forcément avoir des notions sur les réseaux de Petri (qui pourront lui être expliqués) mais une expérience d’utilisation de Coq sera appréciée.

Références

[Coq]: The Coq proof assistant. http://coq.inria.fr.
[CPN-AMI]: CPN-ami online. http://www-src.lip6.fr/logiciels/mars/CPNAMI/.
[LL01]: C. Lakos and G. Lewis. Incremental state space construction of coloured Petri nets. In Proc. 22nd Int. Conf. Application and Theory of Petri Nets (ICATPN’01), Newcastle, UK, June 2001, volume 2075 of Lecture Notes in Computer Science, pages 263–282. Springer, 2001.
[CMP]: C. Choppy and M. Mayero and L. Petrucci. Experimenting formal proofs of petri nets refinements. In Proc.REFINE’08, Turku, Fin, May 2008, volume 214 of Electr. Notes Theor. Comput. Sci., pages 231–254, 2008.

Ce document a été traduit de L^AT_EX par H^EV^EA