The application domains of this thesis are Health Smart Homes, and the research is more precisely centered on the improvement of daily-living for cognitively impaired persons and theirs caregivers.The proposed system can observe the context of each person, personalize the environment and assist the tasks detected if they need to be. Every action of the system is as unobtrusive as possible and takes into consideration the presence of more than one person. To personalize and assist the daily-living activities of a lone person, we need to know his personal context. This context is the conjunction of the preferences and habits, the illness or impairment, the movements in the smart home and the state of the various sensor and electrical devices, and the current activities that are detected for one person. To be able to assist many persons simultaneously, we need to compute the overall conjunction of each and every person's context since every presence can influence the global context and every personal one. This complexity brings a lot of problems like the multiple person localization and identification, or the personalization and assistance of multiple persons in the same space with various activities. Those problems are even more interesting since, following an ethical choice to ensure inhabitant's privacy, this project avoid the use of some intrusive technologies.

Pour s'assurer que les personnes âgées soient en sécurité au domicile, le projet INOVUS s'intéresse aux risques liés à l'utilisation de la cuisinière. Dans le cadre de ce projet, les travaux de M.Sc. présentés dans ce mémoire se concentrent sur la perspective logicielle de la détection et de la prévention des risques physiques pour la personne, lors de la réalisation de tâches utilisant la cuisinière. Dans un premier temps, une revue des risques à domicile recensés dans la littérature a permis de définir la couverture nécessaire à une telle solution. Certaines situations dangereuses ont ensuite été sélectionnées pour définir un modèle de solution satisfaisant. Le développement d'une solution de sécurité pour la personne entraîne des contraintes de fiabilité de très haut niveau pour la technologie produite.Pour répondre à ce besoin, la proposition de ces travaux de M.Sc. est l'utilisation de spécifications formelles. Ces outils permettent d'obtenir un plus haut degré de fiabilité de logiciels. En se basant sur ces outils, un modèle de solution a été élaboré pour le projet INOVUS, et ce à l'aide du vérificateur de modèle ALLOY. Enfin, une implémentation en Java de ce prototype a été réalisée afin d'évaluer les résultats de détection des situations dangereuses. Ce prototype permet alors à la fois de valider l'approche de développement choisie, ainsi que d'établir une preuve de concept d'une telle solution de sécurité.

Le vieillissement actuel de la population provoque un accroissement de problèmes dans les systèmes de santé, dont une pénurie de personnel médical pour les soins à domicile. Le vieillissement de la population a également pour effet d'augmenter le nombre de personnes avec troubles cognitifs. Les comportements incohérents induits par les symptômes des troubles cognitifs limitent la capacité de ces personnes à réaliser leurs activités de la vie quotidienne (AVQ). L'un des axes de recherche prometteurs de cette problématique est l'amélioration et le maintien de la qualité de vie des personnes avec troubles cognitifs dans leurs domiciles. Pour répondre à cette problématique, plusieurs laboratoires de recherche, dont le laboratoire de DOmotique et d'informatique Mobile de l'Université de Sherbrooke (DOMUS), explorent les différents moyens de soutenir, à l'intérieur d'un habitat intelligent, un occupant avec troubles cognitifs dans l'accomplissement de ses AVQ. Cette approche s'inscrit dans le récent courant de pensée issu de l'intelligence ambiante, qui fait référence à une tendance où les environnements sont enrichis avec des technologies (capteurs, effecteurs et autres dispositifs interconnectés par un réseau), dans le but de concevoir un système pouvant planifier une assistance ponctuelle aux occupants en fonction des informations recueillies et de l'historique des données accumulées. L'une des difficultés majeures inhérentes à ce contexte est la reconnaissance et la prédiction des comportements anormaux lorsque les occupants effectuent leurs AVQ à l'intérieur d'un habitat intelligent. Cette thèse vise à contribuer à l'amélioration du processus de reconnaissance de comportements d'un occupant avec troubles cognitifs. Notre proposition consiste en une approche de reconnaissance et prédiction de comportements fondée sur une formalisation des actions basée sur la théorie des possibilités, une alternative à la théorie des probabilités. Les actions sont inférées à partir de l'état actuellement observé de l'habitat intelligent obtenu grâce aux évènements envoyés par les capteurs présents dans l'appartement, lesquelles peuvent fournir une information incomplète et imparfaite. À partir de la séquence d'actions observées plausibles, l'approche proposée utilise une formalisation des activités en structure de plans d'actions pour inférer le comportement observé de l'occupant. Cette approche est en mesure de considérer les comportements erronés, où l'occupant effectue de façon erronée certaines activités tandis que d'autres peuvent être effectuées de façon cohérente, et les comportements cohérents, où l'occupant effectue une ou plusieurs activités de façon cohérente. Les hypothèses sur le comportement observé sont ensuite utilisées pour déterminer les opportunités d'assistance que l'habitat intelligent peut offrir. L'approche proposée a été implémentée et validée au sein de l'infrastructure du projet"Ambient Intelligence for Home-based Elderly Care" à l'"Institute for Infocomm Research" de Singapour et présente des résultats prometteurs pour des scénarios de cas réels effectués dans l'infrastructure. Le développement d'un habitat intelligent capable de maintenir et d'améliorer la qualité de vie des personnes avec troubles cognitifs permettrait de diminuer le fardeau des aidants naturels et professionnels, facilitant le choix des ces personnes de rester à domicile. Ce type de technologie pourrait constituer une solution viable aux problèmes des systèmes de santé associés au vieillissement de la population. De plus, ce type d'approche peut également être utilisé dans des contextes où les comportements anormaux et les situations à risque doivent être évités comme, par exemple, dans le domaine de l'aviation.

La vérification à l’exécution est une méthode formelle légère qui consiste à vérifier qu’une exécution d’un système est correcte par rapport à une spécification. La spécification exprime de manière rigoureuse le comportement attendu du système, en utilisant généralement des formalismes basés sur la logique ou les machines à états finies. Alors que la verification a l’éxecution traite les systèmes monolithiques de manière exhaustive, plusieurs difficultés se présentent lors de l’application des techniques existantes à des systèmes décentralisés, c-à-d. des systèmes avec plusieurs composants sans point d’observation central. Dans cette thèse, nous nous concentrons particulièrement sur trois problèmes : la gestion de l’information partielle, la séparation du déploiement des moniteurs du processus de vérification lui-même et le raisonnement sur la décentralisation de manière modulaire et hiérarchique. Nous nous concentrons sur la notion de spécification décentralisée dans laquelle plusieurs spécifications sont fournies pour des parties distinctes du système. Utiliser une spécification décentralisée a divers avantages tels que permettre une synthèse de moniteurs à partir des spécifications complexes et la possibilité de modulariser les spécifications. Nous présentons également un algorithme de vérification général pour les spécifications décentralisées et une structure de données pour représenter l’exécution d’un automate avec observations partielles. Nous développons l’outil THEMIS, qui fournit une plateforme pour concevoir des algorithmes de vérification décentralisée, des mesures pour les algorithmes, une simulation et des expérimentations reproductibles pour mieux comprendre les algorithmes.Nous illustrons notre approche avec diverses applications. Premièrement, nous utilisons des spécifications décentralisées pour munir une analyse de pire cas, adapter, comparer et simuler trois algorithmes de vérification décentralisée existants dans deux scénarios: l’interface graphique Chiron, et des traces et spécifications générées aléatoirement. Deuxièmement, nous utilisons des spécifications décentralisées pour vérifier diverses propriétés dans un appartement intelligent: correction du comportement des capteurs de l’appartement, détection d’activité spécifiques de l’utilisateur (Activities of Daily Living, ADL) et composition de spécifications des deux catégories précédentes.En outre, nous élaborons sur l’utilisation de spécifications décentralisées pour la vérification décentralisée pendant l’exécution de programmes parallélisés. Nous commençons par discuter les limitations des approches et des outils existants lorsque les difficultés introduites par le parallélisme sont rencontrées. Nous détaillons la description de zones de parallélisme d’une unique exécution d’un programme et décrivons une approche générale qui permet de réutiliser des techniques de verification à l’éxécution existantes. Dans notre configuration, les moniteurs sont déployés dans des fils d’exécution spécifiques et échangent de l’information uniquement lorsque des points de synchronisation définis par le programme lui-même sont atteints. En utilisant les points de synchronisation existants, notre approche réduit les interférences et surcoûts résultant de la synchronisation, au prix d’un retard pour déterminer le verdict. / Runtime Verification (RV) is a lightweight formal method which consists in verifying that a run of a system is correct with respect to a specification. The specification formalizes the behavior of the system typically using logics or finite-state machines. While RV comprehensively deals with monolithic systems, multiple challenges are presented when scaling existing approaches to decentralized systems, that is, systems with multiple components with no central observation point. We focus particularly on three challenges: managing partial information, separating monitor deployment from the monitoring process itself, and reasoning about decentralization in a modular and hierarchical way. We present the notion of a decentralized specification wherein multiple specifications are provided for separate parts of the system. Decentralized specifications provide various advantages such as modularity, and allowing for realistic monitor synthesis of the specifications. We also present a general monitoring algorithm for decentralized specifications, and a general datastructure to encode automata execution with partial observations. We develop the THEMIS tool, which provides a platform for designing decentralized monitoring algorithms, metrics for algorithms, and simulation to better understand the algorithms, and design reproducible experiments.We illustrate the approach with two applications. First, we use decentralized specifications to perform a worst-case analysis, adapt, compare, and simulate three existing decentralized monitoring algorithms on both a real example of a user interface, and randomly generated traces and specifications. Second, we use decentralized specifications to check various specifications in a smart apartment: behavioral correctness of the apartment sensors, detection of specific user activities (known as activities of daily living), and composition of properties of the previous types.Furthermore, we elaborate on utilizing decentralized specifications for the decentralized online monitoring of multithreadedprograms. We first expand on the limitations of existing tools and approaches when meeting the challenges introduced by concurrency and ensure that concurrency needs to be taken into account by considering partial orders in traces. We detail the description of such concurrency areas in a single program execution, and provide a general approach which allows re-using existing RV techniques. In our setting, monitors are deployed within specific threads, and only exchange information upon reaching synchronization regions defined by the program itself. By using the existing synchronization, we reduce additional overhead and interference to synchronize at the cost of adding a delay to determine the verdict.

Résumé : Pour assister efficacement les personnes en perte d'autonomie dans le contexte des habitats intelligents, il est essentiel d'identifier les difficultés auxquelles ces personnes sont confrontées dans leur quotidien. L'objectif de ce travail est d'observer les processus exécutifs durant les activités de la vie quotidienne, ainsi que leur dysfonctionnement lors du vieillissement cognitif (normal ou lié à la maladie d'Alzheimer), puis d'élaborer un modèle théorique et informatique capable de simuler les comportements observés. Une phase d'observation et de qualification des processus de contrôle exécutif (capacités de régulation de l'action, de correction et d'adaptation lors de situations imprévues) a d'abord été réalisée, dornnant lieu à la spécification d'un modèle théorique fondé sur le modèle de contrôle attentionnel de l'action de Norman et Shallice. Le modèle théorique a ensuite été implémenté informatiquement et permet de simuler une activité quotidienne spécifique. // Abstract : In order to assist patients who are loosing their autonomy, smart homes and cognitive assistance systems have to be based on a good knowledge of people's disorders and on the difficulties they are likely to encounter in daily life. The specific objective of this PhD is to observe executive processes involved in the completion of daily activities and their impairment during ageing and dementia of the Alzheimer's type, and then to design both theoretical and computational models which are able to generate the observed behaviours. An observation and a qualification phase, allowing to observe executive control processes (action regulation, correction and adaptation when unexpected situations occur) have been first realized, leading to the specification of a theoretical model based on the Norman and Shallice model. This theoretical model has then been implemented to obtain a computational model, which allows the simulation of a specific activity of daily living.

Après un tour du monde des Habitats Intelligents pour la Santé (HIS), nous décrivons la mise en place du système grenoblois développé au laboratoire TIMC : le Système d'Information Domotique-Santé Intégré à Domicile (SID²). Nous faisons l'hypothèse que les rythmes biologiques et sociaux sont liés au comportement, et donc à l'activité physique, que nous mesurons par le déplacement du sujet d'observation au sein de l'habitat. Nous créons le terme " Rythmes Circadiens d'Activité " (RCA) pour faire référence à la mesure comportementale de l'activité des patients dans l'habitat. Le système SID² est composé d'un HIS externe relié à Internet, et d'un HIS local, objet de ce document. L'HIS local effectue la surveillance multi-paramétrique et auto-apprend les habitudes de vie d'un patient à domicile à travers le calcul des RCA, de façon à détecter une évolution anormale de son comportement sur le long terme. Un simulateur a été développé pour valider le système.

Pour assister efficacement les personnes en perte d'autonomie dans le contexte des habitats intelligents, il est essentiel d'identifier les difficultés auxquelles ces personnes sont confrontées dans leur quotidien. L'objectif de ce travail est d'observer les processus exécutifs durant les activités de la vie quotidienne, ainsi que leur dysfonctionnement lors du vieillissement cognitif (normal ou lié à la maladie d'Alzheimer), puis d'élaborer un modèle théorique et informatique capable de simuler les comportements observés. Une phase d'observation et de qualification des processus de contrôle exécutif (capacités de régulation de l'action, de correction et d'adaptation lors de situations imprévues) a d'abord été réalisée, donnant lieu à la spécification d'un modèle théorique fondé sur le modèle de contrôle attentionnel de l'action de Norman et Shallice. Le modèle théorique a ensuite été implémenté informatiquement et permet de simuler une activité quotidienne spécifique.