Les travaux présentés dans ce document sont orientés vers la vérification formelle de propriétés de sûreté dans le cadre de la conception des systèmes enfouis. Nous nous plaçons dans le formalisme du modèle polyédrique, combinaison des systèmes d'équations récurrentes affines avec les polyèdes entiers. Ce modèle permet de faire de la synthèse de haut niveau pour générer des architectures parallèles à partir de la description d'un système régulier dont les dimensions sont définies par des paramètres symboliques. Nous nous intéressons à la vérification de propriétés de sûreté portant sur des signaux booléens de contrôle, générés ou introduits manuellement lors de la synthèse. Les propriétés sur de tels signaux seront appelées propriétés de contrôle. Nous montrons dans ce document que le modèle polyédrique est adapté pour la vérification formelle de propriétés de contrôle.<br /> Dans ce travail, nous développons une "logique polyédrique" qui nous permet de spécifier et prouver des propriétés dans le modèle polyédrique. La syntaxe et la sémantique des formules logiques s'appuient sur celles d'un langage de description de systèmes d'équations récurrentes affines sur des domaines polyédriques. Les règles de déduction sont de différents types : des règles "classiques" sur les connecteurs logiques, des règles de réécriture et des règles induites par des calculs dans le modèle. Nous développons des algorithmes pour automatiser la construction des preuves, ainsi que des techniques heuristiques permettant d'accélérer cette construction. Ces algorithmes nous permettent de prouver des propriétés simples, comme par exemple la propriété qu'un signal vaut toujours vrai pour un ensemble de processeurs et une durée déterminés. Nous présentons ensuite et commençons à développer des pistes afin d'enrichir notre logique pour exprimer des propriétés plus complexes, comme par exemple des propriétés d'exclusion mutuelle. Nous présentons quelques tactiques de preuve pour ces propriétés plus riches.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00011522 |
| Date | 27 October 2004 |
| Creators | Morin-Allory, Katell |
| Publisher | Université Rennes 1 |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | French |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.0013 seconds