ملخص: 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.

:
لغة: فرنسية
الوصف المادي: 123 p. ill. ;30 cm
الشهادة: Magister
مؤسسة مناقشة الرسالة: Batna, Université du Hadj Lakhdar. Faculté des Sciences de l'Ingénieur
تخصص: Informatique industrielle
الفهرس العشري 511.35 .نظرية التكرار (الأوتوماتة الخلوية ، لامدا-حساب التفاضل والتكامل ، الآلات المتسلسلة ، شبكات بيتري ، نظرية العودية ، نظرية الأتمتة الرياضية ، النظرية الرياضية للآلات ، الأعمال على آلات تورينج)
الموضوع الإعلام الآلي

الكلمات الدالة:
VHDL (langage de description de matériel informatique)
Pétri, réseaux de

ملاحظة: Bibliogr.pp.120-123