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

There is an urgent need to provide qualityof- life (QoL) to a growing population of older adults (OAs) living independently. Solutions that focus on the person and take into account their preferences and context are recognized as key. We introduce a framework for representing and reasoning about the activities of daily living (ADLs) of OAs 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, personalized for each participant according to their preferences and context. Requirements specific to each individual are formulated and encoded in linear temporal logic (LTL), and a model checker is used to verify whether each is satisfied by the model of the participant’s behavior. We demonstrate the framework’s generalizability by applying it to two different participants, highlighting its potential to enhance the safety and well-being of OAs aging in place.