💻 computer science

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

This paper presents a personalized formal verification framework that integrates sensor data with individual context to model and formally verify Activities of Daily Living for older adults living independently, using Linear Temporal Logic to detect safety violations and generate explanatory counterexamples.

Original authors: Ricardo Contreras, Filip Smola, Nuša Farič, Jiawei Zheng, Jane Hillston, Jacques D. Fleuriot

Published 2026-01-15

📖 5 min read🧠 Deep dive

CC BY 4.0

Original authors: Ricardo Contreras, Filip Smola, Nuša Farič, Jiawei Zheng, Jane Hillston, Jacques D. Fleuriot

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine you have a very smart, very patient digital assistant living with an older adult. This assistant doesn't just watch; it tries to understand the person's unique daily rhythm, their preferences, and their home layout. The paper you shared describes a new "rulebook" for building this assistant, using a mix of real-world sensors and formal logic to ensure the person is safe and happy while living independently.

Here is how the framework works, broken down into simple concepts:

1. The Setup: Building a Digital Twin

Think of the older adult's home as a complex puzzle. To understand how the puzzle pieces fit together, the researchers didn't just stick sensors on walls; they first sat down for a chat (a semi-structured interview).

The Interview: They asked the person about their routines, what they like, what they dislike (like privacy concerns in the bedroom), and how they move around.
The Sensors: They installed unobtrusive "digital eyes" (motion sensors) and "digital touch sensors" (contact sensors on doors, drawers, and fridges). These sensors act like the nervous system of the house, sending tiny signals whenever a door opens or someone walks by.
The Result: They combined the chat notes with the sensor data to build a Personalized Digital Twin. This isn't a generic model; it's a custom-made map of that specific person's life and home.

2. The Rulebook: Writing "If-Then" Stories

Once they had the digital twin, they needed a way to check if the person was doing what they usually do. Instead of just looking at raw data, they wrote a "Rulebook" using a special language called Linear Temporal Logic (LTL).

Think of this like writing a story with strict plot points.

Example Rule 1 (The Morning Shower): "Once the person wakes up and leaves the bedroom, they must eventually go to the hallway, then the bathroom, and finally close the shower door."
Example Rule 2 (The Pet Food): "If the fridge is opened in the morning, it must happen before any kitchen cupboards are opened." (This was a specific preference for one participant who feeds their pets before breakfast).
Example Rule 3 (The Medicine): "To get to the medicine, the person must pass through the lounge first."

These rules are written in a precise mathematical language that a computer can read without getting confused.

3. The Judge: The Model Checker

This is where the magic happens. The researchers used a tool called NuSMV, which acts like a super-fast, tireless judge.

The judge takes the Digital Twin (the map of the house and sensors) and the Rulebook (the LTL rules).
It runs through the day's data like a movie reel, checking every single scene against the rules.
If the rule is followed: The judge says, "All clear!"
If the rule is broken: The judge doesn't just say "Error." It prints out a Counter-Example. This is like a "replay" showing exactly where the story went off-script.

4. What They Found (The Results)

The team tested this on two different people (let's call them Participant A and Participant B) to see if the system worked.

The "Almost" Mistake: For Participant A, the rule said: "Bedroom -> Hallway -> Bathroom -> Shower Door Closed." On one morning, the person went Bedroom -> Hallway -> Bathroom -> Hallway -> Bathroom -> Shower Door Closed.
- The computer flagged this as a "violation" because the person went back to the hallway.
- The Insight: The person did take a shower, but their routine had a tiny detour. The system caught this, showing that the rules might need to be slightly more flexible to allow for small, harmless wiggles in the routine.
The "Missed" Step: For Participant B, the rule was about taking medicine. The rule said they must go through the lounge to get the medicine. On one day, the person didn't go through the lounge until after the expected time window.
- The Insight: The system flagged this as a violation. This is important because, unlike a shower, missing a scheduled medication time could be a safety risk. The system successfully identified that the activity happened, but not when it was supposed to.

5. The Bottom Line

The paper claims that this framework is a powerful new way to monitor older adults. It's not just about watching them; it's about understanding their specific context.

It's Personal: It respects privacy (by not using cameras) and adapts to the person's specific home and habits.
It's Precise: It uses math to prove whether a behavior is "safe" or "normal" for that specific person.
It's a Safety Net: It can spot when someone deviates from their routine, whether it's a harmless change (like taking a shower a few minutes later) or a potential warning sign (like forgetting to take medicine).

The researchers conclude that while the system works well, human behavior is messy. Sometimes a sensor sees a fridge open, but we don't know if food was eaten. However, by combining the sensors with the person's own stories and preferences, this framework offers a much clearer, more personalized picture of their daily life than ever before.

Technical Summary: A Personalised Formal Verification Framework for Monitoring Activities of Daily Living

Problem Statement
The paper addresses the urgent need to support the quality of life (QoL) and safety of a growing population of older adults (OAs) living independently. While sensor-based monitoring of Activities of Daily Living (ADLs) is established for detecting health declines, existing approaches often lack personalisation. Many systems rely on generic assumptions about routines and locations, failing to account for individual preferences, specific home layouts, and privacy concerns. Furthermore, previous work utilizing formal methods for ADL monitoring has largely been confined to controlled, simulated environments rather than real-world domestic settings. The core challenge is to develop a system that can rigorously verify whether an individual's observed behaviour adheres to their specific safety and routine requirements without imposing a "one-size-fits-all" model.

Methodology
The authors propose a framework that integrates unobtrusive commercial sensor data with rich contextual information derived from semi-structured interviews and sociological observations. The methodology proceeds through the following stages:

Data Collection:
- Qualitative: Researchers conduct semi-structured interviews to map daily routines, preferences, privacy boundaries, and specific needs. This informs sensor placement and property definition.
- Quantitative: Contact sensors (monitoring doors, drawers, appliances) and passive infrared (PIR) motion sensors are deployed in participants' homes. Data is aggregated via Home Assistant and stored in InfluxDB.
- Participants: The study involved 10 OAs (aged 67–97) in Edinburgh, Scotland. The paper presents detailed case studies of two participants (A and B) with contrasting routines.
Data Preprocessing:
- Sensor data is cleaned to remove noise (e.g., temperature fluctuations in contact sensors) and redundant state updates.
- Motion sensor events are treated as instantaneous transitions, with "clear" states removed unless they mark the end of a movement sequence.
- Data is segmented into 20-minute "subtraces" with 10-minute overlaps to manage the state space explosion problem inherent in model checking.
Formal Modelling:
- Model Generation: An automated tool generates a finite state transition system (using NuSMV) based on the participant's home layout (represented as a directed graph of rooms) and the specific sensor configuration.
- State Representation: The model tracks sensor states (open/closed, detected/clear) and participant movement between rooms.
- Property Specification: Requirements are encoded in Past Linear Temporal Logic (pLTL), an extension of Linear Temporal Logic (LTL) that includes past-time operators. This allows for reasoning about event sequences relative to the current time. Properties are derived from the interview analysis and categorised as general (e.g., hygiene), individual-specific (e.g., pet care), or routine-based (e.g., medication).
Verification:
- The NuSMV model checker verifies if the generated model satisfies the pLTL properties.
- If a property is violated, NuSMV generates a counterexample (a specific sequence of states) to identify the cause of the deviation.

Key Contributions
The paper outlines three primary contributions:

A Comprehensive Framework: It integrates formal model verification with commercial sensor data and explicit contextual information (interviews, home layouts, observations) to create personalised models. This links sensor events directly to individual preferences and needs.
Systematic Specification Approach: It provides a rigorous method for deriving formal properties from semi-structured interviews, ensuring that the verification criteria reflect the unique context of each participant.
Generalisability in Real-World Settings: The framework is demonstrated on two distinct participants with different ADLs, proving its adaptability to diverse living situations and routines outside of controlled laboratory environments.

Results and Analysis
The framework was applied to verify specific morning routines for two participants:

Participant A: Properties verified included a specific sequence for showering (Bedroom $\to$ $\to$ Hallway $\to$ $\to$ Bathroom $\to$ $\to$ Shower Door Closed) and a specific sequence for feeding pets (Refrigerator opened before other cupboards).
- Findings: The shower property was satisfied on most days but violated once due to a minor deviation (returning to the hallway before closing the shower door). The pet-feeding property was violated once on a Sunday, likely due to a shift in weekend routines.
Participant B: A property verified the sequence of moving from the lounge to the kitchen to access a medication dispenser.
- Findings: The property was satisfied on most days but violated on one Friday when the participant accessed the medication after the defined time window (9:50 AM vs. the 7:00–9:00 AM window).

The analysis highlights that while the framework successfully identifies deviations, some "violations" stem from minor, non-critical routine shifts (e.g., taking a shower slightly later or in a different order) rather than safety risks. Conversely, deviations in scheduled medication intake were flagged as potential safety risks. The study also noted limitations, including sensor malfunctions (approx. 1% of data), noise from pets/visitors, and the inherent ambiguity of sensor events (e.g., opening a fridge does not guarantee food consumption).

Significance and Claims
The paper claims that this framework offers a novel, person-centred approach to ADL monitoring that moves beyond generic health alerts. By combining formal verification with qualitative context, the system can:

Detect unanticipated behaviours over time.
Distinguish between routine deviations and potential safety risks.
Provide a mechanism for timely intervention when critical properties (like medication adherence) are violated.

The authors maintain a modest stance, acknowledging that while the framework shows promise for enhancing safety and well-being, challenges remain regarding the interpretation of sensor data and the variability of human behaviour. They conclude that the approach is feasible for real-world deployment but requires careful refinement of temporal requirements to accommodate the natural flexibility of daily life.