Comme les systèmes matériels et logiciels grandissent de façon continue en échelle et fonctionnalités, la probabilité d'erreurs subtiles de- vient toujours plus grande. Les techniques d'abstraction, souvent basées sur l'interprétation abstraite de Cousot, fournissent une méthode pour exécuter symboliquement les systèmes en utilisant le domaine abstrait 'a la place du domaine concret. Dans cette thèse, on introduit des techniques d'abstraction pour les logiques sous des interprétations multivaluées. Beaucoup d'applications des logiques multivaluées ont été trouvées dans la vérification du matériel et du logiciel. Pour la vérification du matériel, des outils de simulation et des réalisations des circuits multivaluées véritables ont été proposés, les risques dynamiques ont été modelés en introduisant des 'états faux pour trouver des régions chevauchantes des signaux en concurrence, etc. Pour la vérification du logiciel on a besoin d'incertitude parce qu'on ne peut savoir si certains comportements devraient être possibles et on a besoin du désaccord parce que l'on peut avoir des acteurs différents qui sont en désaccord pour la manière dont les systèmes devraient se comporter. Les abstractions sont obtenues en appliquant des relations d''équivalence et après, les symboles prédicatifs de la logique sont redéfinis 'a s'appliquer cor- correctement aux classes d''équivalence 'a l'aide des politiques d'interprétation. On fournit des résultats de préservation pour la logique de premier ordre, pour la logique temporelle et pour la logique temporelle de la connaissance. Avant de discuter les abstractions multivaluées pour la logique temporelle, nous présentons une 'étude de cas pour utiliser l'abstraction dans le contexte des modèles du contrôle d'accès. Nous fournirons aussi une technique d'abstraction pour les types de données. Cette technique d'abstraction peut être 'élargie pour les types abstraits de données. Ici, les abstractions sont appliquées aux spécifications initiales au moyen des 'équations et ils sont appelés des abstractions 'équationnelles. De plus, la technique d'abstraction présentée généralise et clarifie la nature de beaucoup de techniques d'abstraction trouvées dans la littérature, telles: la technique de dupliquer les symboles prédicatifs, shape analysis, l'abstraction par prédicats, l'approche de McMillan, etc. Pour raisonner au sujet des systèmes dynamiques, on introduit les types de données dynamiques et on étend la méthode d'abstraction antérieure 'a ce cas. Le problème principal qui survient quand on utilise les abstractions est de trouver l'abstraction convenable ou de raffiner une abstraction déjà existante pour en obtenir une meilleure. On prouve que les techniques d'abstraction que nous avons introduites pour les types de données sous interprétation 3- valu'ee Kleene, peuvent être utilisées dans une procédure de raffinement. De plus, on montre que la procédure de raffinement guide par contre-exemple est plus efficace quand on l'utilise sous les abstractions 'équationnelles.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00623170 |
| Date | 08 January 2008 |
| Creators | Enea, Constantin |
| Publisher | Université Paris-Est |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | English |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.002 seconds