Résumé: 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:
Langue: Français
Collation: 150 p. ill. ;30 cm.
Diplôme: Doctorat
Etablissement de soutenance: Grenoble, Institut National Polytechnique
Spécialité: Informatique
Index décimal 621 .Physique appliquée (électrotechnique, génie civil, génie mécanique, ingénierie appliquée, principes physiques en ingénierie)
Thème Informatique

Mots clés:
machine d'état finis
Systéme matériels numérique
vérification fonctionnelle

Note: Bibliogr. pp.137-144; Annexe pp.145-150