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

TL;DR

This paper presents a personalised formal verification framework that models and checks activities of daily living for older adults living independently, aiming to improve safety and well-being through sensor data and formal methods.

Contribution

It introduces a novel framework integrating sensor data and contextual information to create personalised formal models for monitoring older adults' activities.

Findings

Framework successfully models individual preferences and contexts.

Model checking verifies safety properties for each participant.

Counterexamples identify causes of activity violations.

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.