ملخص: La validation fonctionnelle d'un système matériel consiste à vérifier le système vis-à-vis de son fonctionnement attendu. Il existe deux façons de spécifier ce fonctionnement attendu. D'une part, la spécification peut être donnée sous forme d'une description fonctionnelle complète. d4autre part, l'expression de cette spécification peut être donnée sous forme d'un ensemble de propriétés temporelles critiques. Ces deux façon de spécifier les systèmes matériels ont donnée lieu à deux problèmes de vérification. Notre domaine d'étude concerne les systèmes matériels numériques séquentiels synchrones. Ce document développe une approche de vérification se ramène à définir une machine d'états finis sur laquelle la vérification sera réalisée. L'application du langage Lustre et de l'outil de vérification Lesar associé a été étudiée dans le but de valider cette approche. Dans cette application, la résolution des deux problèmes de vérification consiste à vérifier que cette sortie est la constante booléenne. Cette vérification est réalisée automatiquement par l'outil de vérification Lesar.

Grenoble:
لغة: فرنسية
الوصف المادي: 150 p. ill. ;30 cm.
الشهادة: Doctorat
مؤسسة مناقشة الرسالة: Grenoble, Institut National Polytechnique
تخصص: Informatique
الفهرس العشري 621 .الفيزياء التطبيقية (الهندسة الكهربائية ، الهندسة المدنية ، الهندسة الميكانيكية ، الهندسة التطبيقية ، المبادئ الفيزيائية في الهندسة)
الموضوع الإعلام الآلي

الكلمات الدالة:
machine d'état finis
Systéme matériels numérique
vérification fonctionnelle

ملاحظة: Bibliogr. pp.137-144; Annexe pp.145-150