Dieses Dokuwiki verwendet ein von Anymorphic Webdesign erstelltes Thema.

Différences

Ci-dessous, les différences entre deux révisions de la page.

Lien vers cette vue comparative

Les deux révisions précédentes Révision précédente
projet_syncomp [2009/09/23 17:48]
tigli
projet_syncomp [2009/09/23 17:49] (Version actuelle)
tigli
Ligne 13: Ligne 13:
 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 :  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 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)   * 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 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 ​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 œ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. 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.
projet_syncomp.txt · Dernière modification: 2009/09/23 17:49 par tigli
Piste:
Dieses Dokuwiki verwendet ein von Anymorphic Webdesign erstelltes Thema.
CC Attribution-Noncommercial-Share Alike 3.0 Unported
www.chimeric.de Valid CSS Driven by DokuWiki do yourself a favour and use a real browser - get firefox!! Recent changes RSS feed Valid XHTML 1.0