Verifying properties of activities of daily living

The monitoring of Activities of Daily Living (ADLs) for older adults can support their well-being since deviations in behaviour may indicate cognitive or physical decline, and reduced quality-of-life. In this work we present a new methodology that combines the spatial context with the observed behaviour of the person to enable a rigorous analysis of their daily activities. Tailored models are constructed that capture the layout of the individual’s home and incorporate timestamped data from unobtrusive sensors attached to everyday objects. We specify expected behaviours as properties encoded in linear temporal logic and use model checking to assess whether sensor-captured behaviours align with expectations. Importantly, our methodology is agnostic to different forms of ADLs and behaviour specifications.