Auteur
BOUBEZARI, Abderrahim
Directeur de thèse
Ben Yelles Choukri-Bey (Professeur)
Filière
Informatique
Diplôme
Magister
Titre
Transcription des réseaux de Petri dans le système FoCaLiZe
Mots clés
Pétri, Réseaux de : Transcription ; Méthodes formelles (informatique) ; Logique du premier ordre ; Théorèmes : Démonstration automatique ; Logique mathématique
Résumé
Les méthodes formelles sont des techniques qui permettent de vérifier et de valider mathématiquement des logiciels informatiques. Il existe plusieurs types de méthodes formelles, différents selon les modélisations du système à valider et les outils utilisés pour y parvenir. Une première approche formelle présentée est celle basée sur la démonstration mathématique de propriétés relatives au système spécifié. Elle est mise en oeuvre par des langages formels tel que le système FoCaLiZe. C’est un atelier de programmation certifiée dans lequel il est possible de spécifier, programmer et prouver la correction du programme vis-à-vis de la spécification de départ. Pour cela, un développement FoCaLiZe est basé sur deux constructions principales : les espèces et les collections. Une espèce sert à implanter des méthodes pour manipuler des éléments d’un type support. Une espèce subit ensuite des raffinements successifs grâce à des mécanismes particuliers comme l’héritage et le paramétrage, et dont le dernier niveau est une collection, destinée à l’utilisateur final. FoCaLiZe dispose de deux outils d’aide à la preuve dans la démonstration des propriétés, que sont le prouveur automatique Zenon pour assister le concepteur, et l’outil d’aide à la preuve Coq pour valider la preuve obtenue grâce à Zénon. Les réseaux de Petri correspondent à un autre type de méthode formelle de modélisation, basé sur la représentation graphique. Il permet de modéliser un système et d’analyser son modèle selon des propriétés spécifiques pour prévenir son comportement futur. Concrètement, un réseau de Petri est un graphe orienté composé de deux types de sommets : les places et les transitions, reliés entre eux par des arcs. Les places représentent les variables d’état du système à modéliser, alors que les transitions représentent les événements qui entraînent ses changements d’état. Nous proposons une démarche de transcription des réseaux de Petri ordinaires dans le système FoCaLiZe. Cette démarche nous permettra d’utiliser ensuite les techniques de preuve offertes par FoCaLiZe pour vérifier des propriétés des réseaux de Petri. Notre démarche consiste en la dérivation de chacun des composants des réseaux de Petri (places, transitions et arcs) en une espèce FoCaLiZe, dont les types support représentent les attributs des composants (identifiants, marquage, poids), et les fonctions servent à les manipuler ces attributs. D’autres espèces sont définies pour représenter les ensembles de composants grâce à la bibliothèque des ensembles finis de FoCaLiZe. Finalement toutes ces espèces sont regroupées dans une espèce globale qui définit la structure générale des réseaux de Petri. Enfin, les propriétés des réseaux de Petri sont traduites en des propriétés ou théorèmes FoCaLiZe, puis prouvées grâce aux outils de preuve associés. A titre d’exemple, nous avons dérivé la propriété de raffinement des réseaux de Petri ordinaires, que nous avons prouvée en utilisant le prouveur Zenon.
Date de soutenance
30/06/2012
Cote
005.14
Pagination
77 p.
Illusatration
ill.
Format
30 cm.
Notes
Support papier accompagné d'un CD-Rom ; Bibliogr. p. 73-77
Statut
Traitée