A Personalised Formal Verification Framework for Monitoring Activities of Daily Living of Older Adults Living Independently in Their Homes
This work addresses the need for personalised monitoring solutions to improve quality of life for older adults living at home, representing an incremental advancement in applying formal methods to this domain.
The paper tackles the problem of monitoring Activities of Daily Living for older adults living independently by developing a personalised formal verification framework that integrates sensor data and contextual information to create individual models and verify properties using Linear Temporal Logic, demonstrating generalisability across participants to enhance safety and well-being.
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.