Proposition de thèses LE2I - Dijon - 2009/2010
Par Sylvain Rampacek le vendredi 25 septembre 2009 à 12h36
Dans le cadre du projet transversal Checksem, l’équipe Systèmes d’informations et systèmes d’imaged du LE2I (Dijon) propose plusieurs sujets de thèse pour la rentrée 2009. Vous pouvez retrouver d’autres sujets sur le site web de CheckSem.
Sujet : CHECKSEM – méthodes et outils pour la qualification de graphes sémantiques
Responsables :
– Christophe Nicolle (cnicolle[AT]u-bourgogne[POINT]fr)
– Sylvain Rampacek (sylvain.rampacek[AT]u-bourgogne[POINT]fr)
Laboratoire : LE2I (Laboratoire Electronique, Informatique et Image), UMR CNRS 5158, Université de Bourgogne.
Équipe : Informatique, cellule "Systèmes d’informations et systèmes d’image" (SISI)
Domaine : Informatique, semantic web, model checking
Information sur le projet CheckSem : http://iutdijon.u-bourgogne.fr/checksem/
Candidature : les candidatures sont à envoyées sur nos adresses mails avant le 30 septembre 2009.
Documents à nous fournir pour postuler : CV détaillé, lettre de motivation, lettres de recommandation (éventuellement), relevé de notes + classement des 2 années de master, le tout par mail à Sylvain Rampacek (sylvain.rampacek[AT]u-bourgogne[POINT]fr) et Christophe Nicolle (cnicolle[AT]u-bourgogne[POINT]fr).
Description détaillée du sujet :
Les Systèmes d’Information Web fournissent un médium de communication riche permettant l’échange rapide et flexible de données structurées. La signification de ces données est décrite habituellement sous forme de graphes sémantiques, c’est-à-dire d’ensembles de triplets sujet-prédicat-objet permettant de représenter les relations entre différentes entités. La norme RDF (Resource Description Framework) forme la base de l’ensemble des langages ontologiques actuellement définis pour la description et la manipulation des données dans le Web sémantique.
Lors de la construction et de l’interconnexion des graphes sémantiques, qui sont de grande taille, il est nécessaire de s’assurer que les données représentées par ces graphes sont cohérentes, ceci revient à vérifier que les graphes respectent certaines propriétés structurelles. Autrement dit, il s’agit de qualifier les graphes sémantiques afin de garantir leur exploitation correcte par les applications. Un moyen efficace d’effectuer cette qualification est d’avoir recours aux techniques de vérification formelle issues du domaine des systèmes parallèles et distribués, notamment la vérification par logiques temporelles (model checking) et par équivalences (equivalence checking). A l’origine, ces techniques ont été conçues pour exprimer et vérifier des propriétés de bon fonctionnement sur les espaces d’états accessibles (systèmes de transitions étiquetées) des programmes parallèles.
Dans le cadre de la plateforme Web CheckSem, notre objectif est de concevoir des méthodes et des outils adaptés à la qualification des graphes sémantiques (RDF) en utilisant les techniques de vérification formelle telles que celles fournies par la boîte à outils CADP (Construction and Analysis of Distributed Processes) développée à l’INRIA. Comme la quasi-totalité des langages du Web sémantique sont traduisibles vers RDF, les outils et méthodes que nous développerons dans cette thèse pourront être étendus à l’ensemble de ces langages.
Le candidat doit avoir des bases solides en programmation. Une bonne connaissance des langages JAVA et C/C++, ainsi que de Linux est essentielle. Des connaissances en web semantic ou model checking serait un plus.
