Résumé: La conception de systèmes de commande spécifique est devenue une tâche actuellement pratiquement automatique. Des outils de plus en plus développés ont été conçues pour aider les concepteurs de contrôleurs dédiés. La conception démarre à partir d’une spécification algorithmique du circuit à oncevoir, un compilateur comportemental fournira en sortie une description RTL du circuit à concevoir, d’autre compilateurs vont fournir par la suite jusqu’à la description du masque du circuit. Dans le cadre cette thèse, on s’intéresse au niveau comportemental, la spécification fournie par le concepteur est simulée pour valider cette spécification. Actuellement, en essaye d’utiliser des outils formels pour vérifier quelques propriétés au niveau de cette spécification initiale. Les réseaux de Petri constituent aujourd’hui l’un des modèle les plus utiliser pour la modélisation du comportement dynamique des systèmes discrets. Dans ce travail, on essaye donc d’utiliser ces réseaux pour valider certains aspects de la spécification. Il s’agit donc de proposer un outil de vérification basé sur ses réseaux de Petri : on part d’une spécification d’un contrôleur dédié décrit dans un langage de spécification de matériel (VHDL), une première compilation est faite pour vérifier certaines erreurs, la sortie sera traduite sous forme d’un réseau de Petri, qui sera par la suite simulé dynamiquement pour vérifier d’autre types d’erreurs. Cet outil est un modèle formel basé sur les réseaux de Petri interprétés, adapté à la représentation des spécifications comportementales des contrôleurs décrit en VHDL, et un modèle de simulation dirigé par événements pour la simulation du modèle représentant la spécification. Les résultats sont analysés en appliquant quelques propriétés relatives au formalisme des réseaux de Petri pour détecter quelques éventuelles erreurs de spécifications qui ne peuvent être détectées dans la compilation.

:
Langue: Français
Collation: 123 p. ill. ;30 cm
Diplôme: Magister
Etablissement de soutenance: Batna, Université du Hadj Lakhdar. Faculté des Sciences de l'Ingénieur
Spécialité: Informatique industrielle
Index décimal 511.35 .Théorie de la récurrence (automates cellulaires, lambda-calcul, machines séquentielles, réseaux de Petri, théorie de la récursivité, théorie mathématique des automates, théorie mathématique des machines, travaux sur les machines de Turing)
Thème Informatique

Mots clés:
VHDL (langage de description de matériel informatique)
Pétri, réseaux de

Note: Bibliogr.pp.120-123