Skip to content

Model Checking

Paper on Integrated Technologies of Care published in Nature Scientific Reports

    Our paper titled “Integrated technologies of care: proof-of-concept study on an integrated physiological and activity monitoring system to enhance independence and care” has just been published by Nature Scientific Reports. You can access it here. The showcases work done as part of the Advanced Care Research Centre (ACRC).

    Abstract

    This study presents a multi-sensor activity monitoring system designed to verify daily behaviours and detect physiological anomalies within a controlled home environment. Seven subjects participated in a scripted routine of Activities of Daily Living carried out in a home-like environment. The proposed system is designed for single-occupancy environments (e.g. individuals living alone). Accordingly, this proof-of-concept evaluation was conducted under controlled, single-participant conditions using sequential, non-concurrent activities and excluding overlapping sensor changes. Within the routine, different sensors capture physiological hydration levels and breathing rates of the participant as sensor events, to check whether the measurements were within normal levels. In addition, camera, contact, motion and pressure sensors are used to capture action triggered events within the routine. Sensor data is processed and translated into a time-ordered trace of events. A model is constructed to capture the layout of the controlled environment and the trace of events. Expected behaviours are specified as properties encoded in Linear Temporal Logic and model checking is used to assess whether the sensor-captured events align with these expectations. Through model checking, the captured behaviour can be verified against a set of logical formulae representing properties. The identified deviations from expected behaviours demonstrate the viable application of model checking in the verification of Activities of Daily Living. Cross-sensor data aggregation compensates for occasional sensor inaccuracy, ensuring reliability. The initial results support the system’s potential for use in behaviour and physiological monitoring of people living independently, where accurate and unobtrusive monitoring is crucial.

    Our paper on understanding the ADL of older adults has been published by IEEE Sensors

      Our paper describing “A Personalised Formal Verification Framework for Monitoring Activities of Daily Living of Older Adults Living Independently in Their Homes” has been published by the journal  IEEE Sensors. This describes a novel approach and framework integrating symbolic modelling and data from sensors for understanding the Activities of Daily Living (ADLs) of older adults living independently in their homes in Edinburgh and its neighbourhood.

      The work is part of the Integrated Technologies of Care workpackage of the Advanced Care Research Centre (ACRC).

      Abstract:

      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.
      Print ISSN: 1530-437X
      Online ISSN: 1558-1748
      DOI: 10.1109/JSEN.2025.3635781
      More information available here.