Composition et Validation formelle dans une plateforme d'assemblage de services pour dispositifs
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 SynComp.
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 :
Ces approches permettront à l'étudiant de se familiariser avec l'utilisation du logiciel récent et éprouvé de “model-checking” : 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é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.
Annie Ressouche : +33 4 92 38 79 44 Jean-Yves tigli : +33 6 84 24 55 67