A personalised formal verification framework for monitoring activities of daily living of older adults living independently in their homes

There is an urgent need to provide quality-of-life to a growing population of older adults living independently. Solutions that focus on the person and take into account their preferences and context are recognised as key. 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 data from participants derived from semi-structured interviews, home layouts and additional contextual information, such as the researchers’ observations. These data are used to create formal models, personalised for each participant according to their preferences and context. Requirements specific to each individual are formulated and encoded in Linear Temporal Logic, and a model checker is used to verify whether each is satisfied by the model of the participant’s behaviour. We demonstrate the framework’s generalisability by applying it to two different participants, highlighting its potential to enhance the safety and well-being of older adults ageing in place.