La vérification symbolique de systèmes matériels est limitée par la complexité exponentielle en taille de représentation du modèle symbolique sous-jacent. <br />Ce travail porte sur la réduction, manuelle ou non, de ce modèle. Les approches compositionnelles structurelles et comportementales ont été étudiées dans un contexte industriel. Cette étude a précédé le développement d'une nouvelle technique de réduction : la partition fonctionnelle. Cette technique s'applique aux systèmes dont le comportement est séquentiellement décomposable. La partition fonctionnelle est mise en place grâce à une étape préliminaire de simulation symbolique. Elle a été implémentée et appliquée sur un circuit industriel de taille importante, et a permis d'obtenir d'excellents résultats en matière de réduction. L'expérimentation des techniques de preuve présentées s'est appuyée sur un outil d'extraction de machines d'états finis à partir de descriptions VHDL qu'il a été nécessaire de mettre en œuvre.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00003667 |
| Date | 07 October 2003 |
| Creators | Dumitrescu, E. |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | French |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.0019 seconds