La validation fonctionnelle d'un système matériel consiste a vérifier le système vis-a-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. D'autre 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çons de spécifier les systèmes matériels ont donne lieu a deux problèmes de vérification. Notre domaine d'étude concerne les systèmes matériels numériques séquentiels synchrones. Le travail présente dans ce document développe une approche de vérification unifiée, fondée sur le modèle de machines d'états finis, pour résoudre les deux problèmes de vérification sur ces systèmes. Dans cette approche, tout probleme de vérification se ramène a 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 associe a été étudiée dans le but de valider cette approche. Dans cette application, la resolution des deux problèmes de vérification se ramène a définir un programme lustre ayant une seule sortie. La vérification consiste a vérifier que cette sortie est la constante booléenne 1. Cette vérification est réalisée automatiquement par l'outil de vérification Lesar
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00340909 |
| Date | 02 October 1992 |
| Creators | Berkane, Bachir |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | French |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.0022 seconds