Outils pour utilisateurs
projet_syncomp
Différences
Ci-dessous, les différences entre deux révisions de la page.
| Les deux révisions précédentes Révision précédente Prochaine révision | Révision précédente | ||
|
projet_syncomp [2009/09/23 15:48] tigli |
projet_syncomp [2009/09/23 17:49] (Version actuelle) tigli |
||
|---|---|---|---|
| Ligne 1: | Ligne 1: | ||
| ====== Projet SI5 : SynComp ====== | ====== Projet SI5 : SynComp ====== | ||
| - | {{ wcomp_desing.jpg?300|}} | + | {{ wcomp_desing.jpg?200|}} |
| === Date: 2008-2009 === | === Date: 2008-2009 === | ||
| Ligne 11: | Ligne 11: | ||
| Ce projet s'inscrit dans le cadre d'une collaboration entre l'équipe Pulsar et Rainbow pour la validation formelle de composition de services pour dispositifs, qui a donné lieu à une Action Color de 2007 à 2008 [[http://www-sop.inria.fr/pulsar/projects/SynComp/reunion1.html|SynComp]]. | Ce projet s'inscrit dans le cadre d'une collaboration entre l'équipe Pulsar et Rainbow pour la validation formelle de composition de services pour dispositifs, qui a donné lieu à une Action Color de 2007 à 2008 [[http://www-sop.inria.fr/pulsar/projects/SynComp/reunion1.html|SynComp]]. | ||
| - | Fort des premiers résultats de cette action, le projet consiste maintenant à complèter la plateforme WComp avec une série d'extension logicielles telles que : | + | Fort des premiers résultats de cette action, le projet consiste maintenant à compléter la plateforme WComp avec une série d'extensions logicielles telles que : |
| - | * de nouvelles librairies de composants dotées d'une sémantique formelle qui permettront de vérifier des assemblages de services pour dispositifs (ces librairies permetttront à l'utilisateur d'assembler graphiquement des composants et des services pour dispositifs dans le but de réaliser une application d'informatique ambiante, tout en permettant la vérification de nombreuses propriétés de l'assemblage et de l'application) | + | * de nouvelles librairies de composants dotées d'une sémantique formelle qui permettront de vérifier des assemblages de services pour dispositifs (ces librairies permettront à l'utilisateur d'assembler graphiquement des composants et des services pour dispositifs dans le but de réaliser une application d'informatique ambiante, tout en permettant la vérification de nombreuses propriétés de l'assemblage et de l'application) |
| - | * des mécanismes de c omposition validés entre plusieurs de ces assemblages (ces mécanismes permettront dans le cas de la mise en oeuvre simultamée de plusieurs applications de résoudre avec une logique prouvée les conflits d'accès qui pourraient apparaitre sur les dispositifs de l'application) | + | * des mécanismes de composition validés entre plusieurs de ces assemblages (ces mécanismes permettront dans le cas de la mise en œuvre simultanée de plusieurs applications de résoudre avec une logique prouvée les conflits d'accès qui pourraient apparaître sur les dispositifs de l'application) |
| - | Ces approches permettront à l'étudiant de se familiariser avec l'utilisation du logiciel récent et éprouvé de "model-checking" : [[http://nusmv.irst.itc.it/|NuSMV]] .Ce dernier est un outil efficace mettant en oeuvre deux techniques complémentaires et puissantes de model-checking: la vérification symbolique de propriétés ( formules de logique “temporelle”) et le model-checking borné qui utilise des techniques de SAT-solver pour effectuer la validation de formules logiques. C'est ainsi que ce logiciel nous permettra de prouver de façon exhaustive des propriétés de sureté de fonctionnement et de vivacité de l'appication considérée. | + | Ces approches permettront à l'étudiant de se familiariser avec l'utilisation du logiciel récent et éprouvé de "model-checking" : [[http://nusmv.irst.itc.it/|NuSMV]] .Ce dernier est un outil efficace mettant en œuvre deux techniques complémentaires et puissantes de model-checking: la vérification symbolique de propriétés (formules de logique “temporelle”) et le model-checking borné qui utilise des techniques de SAT-solver pour effectuer la validation de formules logiques. C'est ainsi que ce logiciel nous permettra de prouver de façon exhaustive des propriétés de sureté de fonctionnement et de vivacité de l'application considérée. |
| - | Les résutltats de ce projet feront l'objet d'exprimentations sur la plateforme WComp, dans le cadre de l'Ubiquarium de Polytech et pourront etre valorisé dans le cadre d'une publication scientifique. | + | Les résultats de ce projet feront l'objet d'expérimentations sur la plateforme WComp, dans le cadre de l'Ubiquarium de Polytech et pourront être valorisé dans le cadre d'une publication scientifique. |
| - | + | ||
| - | [1] The NuSMV model-checker: http://nusmv.irst.itc.it/ | + | |
| * ** Un stage est envisageable après le projet** | * ** Un stage est envisageable après le projet** | ||
projet_syncomp.1253713714.txt.gz · Dernière modification: 2009/09/23 15:48 par tigli
Outils de la page
Sauf mention contraire, le contenu de ce wiki est placé sous les termes de la licence suivante : CC Attribution-Noncommercial-Share Alike 4.0 International
