Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Personalised Formal Verification Framework for Monitoring Activities of Daily Living of Older Adults Living Independently in Their Homes

Ricardo Contreras, Filip Smola, Nuša Farič, Jiawei Zheng, Jane Hillston, Jacques D. Fleuriot

TL;DR

The paper presents a personalised formal verification framework for monitoring Activities of Daily Living (ADLs) of older adults living independently at home by fusing sensor data with contextual information obtained from interviews and home layouts. It encodes participant-specific behavioural properties in $LTL$ (via $pLTL$) and verifies them with NuSMV, generating counterexamples when violations occur. The approach realises a data-processing pipeline that includes qualitative analysis, sensor data preprocessing, automated model generation, and property specification, validated on real-world data from 10 participants. Results indicate the framework can identify deviations in routines and highlight safety-relevant issues, demonstrating the potential to enhance safety and QoL for older adults aging in place, while acknowledging challenges in interpretation and timing variability.

Abstract

There is an imperative need to provide quality of life to a growing population of older adults living independently. Personalised solutions that focus on the person and take into consideration their preferences and context are key. In this work, we introduce a framework for representing and reasoning about the Activities of Daily Living of older adults living independently at home. The framework integrates data from sensors and contextual information that aggregates semi-structured interviews, home layouts and sociological observations from the participants. We use these data to create formal models, personalised for each participant according to their preferences and context. We formulate requirements that are specific to each individual as properties encoded in Linear Temporal Logic and use a model checker to verify whether each property is satisfied by the model. When a property is violated, a counterexample is generated giving the cause of the violation. We demonstrate the framework's generalisability by applying it to different participants, highlighting its potential to enhance the safety and well-being of older adults ageing in place.

A Personalised Formal Verification Framework for Monitoring Activities of Daily Living of Older Adults Living Independently in Their Homes

TL;DR

The paper presents a personalised formal verification framework for monitoring Activities of Daily Living (ADLs) of older adults living independently at home by fusing sensor data with contextual information obtained from interviews and home layouts. It encodes participant-specific behavioural properties in (via ) and verifies them with NuSMV, generating counterexamples when violations occur. The approach realises a data-processing pipeline that includes qualitative analysis, sensor data preprocessing, automated model generation, and property specification, validated on real-world data from 10 participants. Results indicate the framework can identify deviations in routines and highlight safety-relevant issues, demonstrating the potential to enhance safety and QoL for older adults aging in place, while acknowledging challenges in interpretation and timing variability.

Abstract

There is an imperative need to provide quality of life to a growing population of older adults living independently. Personalised solutions that focus on the person and take into consideration their preferences and context are key. In this work, we introduce a framework for representing and reasoning about the Activities of Daily Living of older adults living independently at home. The framework integrates data from sensors and contextual information that aggregates semi-structured interviews, home layouts and sociological observations from the participants. We use these data to create formal models, personalised for each participant according to their preferences and context. We formulate requirements that are specific to each individual as properties encoded in Linear Temporal Logic and use a model checker to verify whether each property is satisfied by the model. When a property is violated, a counterexample is generated giving the cause of the violation. We demonstrate the framework's generalisability by applying it to different participants, highlighting its potential to enhance the safety and well-being of older adults ageing in place.

Paper Structure

This paper contains 17 sections, 8 equations, 4 figures, 4 tables.

Table of Contents

  1. Introduction
  2. Related Work
  3. Framework Components and Data Collection
  4. Framework Overview
  5. Data Collection Process
  6. Qualitative Data
  7. Sensor Data
  8. Practical Considerations in Sensor Deployment
  9. Data Processing and Models
  10. Preprocessing
  11. Information from participants
  12. Sensors
  13. Model generator
  14. Formalism and Property Specification
  15. Behaviour-related Properties for Participants
  16. ...and 2 more sections

Figures (4)

  • Figure 1: Main components of the framework.
  • Figure 2: Concrete and abstract layouts of a participant's home. (a) Floorplan for a participant. (b) Graph representing the layout
  • Figure 3: Sensors installed in participants' home kitchens. (a) Motion sensor medication. (b) Contact sensors on drawers.
  • Figure 4: Subtrace for the activation and deactivation of three sensors between time markers $a$ and $b$.