// Soutenance de thèse

Soutenance de thèse de Mohamed HILIA

Intitulé : Canevas Sémantique & Méthodologie Formelle pour le Développement des Applications Ambiantes Multi-domaine
Date : Lundi 16 Décembre 2013 à 10h.
Lieu : Amphithéâtre R&T, Département Réseaux & Télécoms, Vitry-sur-Seine.

Jury

  • Khalil Drira (Directeur de recherche au LAAS de Toulouse)
  • Salima Benbernou (Professeure à l'Université Paris Descartes)
  • Claude Godart (Professeur à l'Université de Lorraine)
  • Kamel Barkaoui (Professeur au CNAM Paris)
  • Dimitris Plexousakis (Professeur a l'Université de Crête)
  • Abdelghani Chibani (Maître de conférences à l'Université Paris-Est Créteil)
  • Karim Djouani (Professeur  à l'Université Paris-Est Créteil), Directeur de thèse
  • Yacine Amirat (Professeur à l'Université Paris-Est Créteil), Co-directeur de thèse
  • Thierry Winter (Directeur de recherche à Bull-Evidian)

Résumé

L'intelligence ambiante est considérée comme l'une des évolutions majeures de l'informatique ubiquitaire. Elle vise la mise en œuvre d’applications dans des environnements dits ambiants ou des espaces intelligents pour améliorer la vie quotidienne des utilisateurs, leur bien-être et leur sécurité. Un environnement ambiant dispose d'une multitude d'équipements (capteurs, actionneurs, robots), fournissant des services ubiquitaires atomiques qui sont distribués et hétérogènes. Ces services atomiques, disponibles dans ce type d'environnement, ne répondent généralement pas aux exigences et besoins des utilisateurs. Pour ce faire, des services composites de haut niveau impliquant l'interaction de services ubiquitaires fournis et/ou contrôlés par différents domaines (i.e. environnement multi-domaine) doivent alors être considérés. Les travaux de cette thèse concernent l'agrégation (coopération et composition) des services ubiquitaires atomiques dans un environnement ambiant multi-domaine. Plus précisément, il s’agit de traiter la problématique de l'interopérabilité sémantique et comportementale des compositions de services ainsi que leurs spécifications dans un modèle formel basé sur la logique constructive BCDL0. Dans cette thèse, nous présentons un canevas sémantique permettant la spécification et la vérification formelles des processus coopératifs en s’appuyant sur l'assistant de preuve Isabelle/HOL. Le canevas proposé consiste en une ontologie de coopération extensible et en un langage de spécification de services fiables « Sound », auxquels s’joutent des modules de mise en correspondance vers des infrastructures cibles. Pour la validation du canevas, un scénario de rééducation d’une personne âgée à domicile, impliquant plusieurs domaines (maison intelligente équipée d’un robot compagnon, hôpital, centre de kinésithérapie) est étudié et mis en œuvre.