Modélisation et spécification formelle de contexte et sa prédiction dans les systèmes diffus : une approche basée sur la logique temporelle et le modèle stochastique

摘要

Depuis son introduction par Mark Weseir, l’informatique omniprésente ne cesse de solliciter de l’intérêt croissant dans la sphère de l’innovation technologique. Soutenue par l’évolution technologique des systèmes embarqués, la miniaturisation et l’intégration de divers dispositifs communicants dans les applications informatiques, cette vision d’une technologie invisible, distribuée et intelligente devient de plus en plus concrète. Dépassant ainsi, les systèmes classiques vers des systèmes omniprésents sensibles à leurs contextes assistant d’une manière active et intelligente ses usagers. En leur apportant aide et commodité dans l’accomplissement des activités quotidiennes, et ce dans différents domaines.ududMettre en place ces systèmes omniprésents proactifs, intelligents et permettant une utilisation adaptée, naturelle et conviviale soulève encore beaucoup de défis pour assurer une proactivité sensible au contexte et adéquate au besoin de l’utilisateur. La majorité des travaux sur l’omniprésence se sont concentrés sur le contexte actuel. Par contre une nouvelle tendance appuie l’idée de l’importance de prendre en considération l’évolution du contexte pour prévoir un contexte futur et permettre de fournir une adaptation active et rapide à des situations futures. Montrant aussi l’importance de développer un cadre formel et général pour le contexte et la prédiction, sauf que jusque-là les approches formelles de la prédiction du contexte général sont manquantes.ududCe travail s’inscrit dans ce cadre. Et il porte sur le formalisme du contexte et la prédiction du contexte dans les systèmes omniprésents proactifs. Il vise à spécifier et modéliser le contexte et la prédiction du contexte futur dans un cadre formel tenant compte de l’évolution temporelle logique de l’espace de service. En premier lieu, nous avons défini le contexte sous une vision multidimensionnelle respectant une logique d’évolution spatiotemporelle. En second lieu, nous avons spécifié et modélisé le contexte dans un cadre formel logique intégrant la dimension spatiotemporelle. À la fin, nous avons spécifié et modélisé la prédiction de contexte futur dans un cadre formel et logique et sous une vision multidimensionnelle, dynamique et non déterministe basée sur la logique PCTL et le modèle de vérification stochastique.