💻 computer science

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

Este artículo presenta un marco de verificación formal personalizado que integra datos de sensores con el contexto individual para modelar y verificar formalmente las Actividades de la Vida Diaria de adultos mayores que viven de forma independiente, utilizando la Lógica Temporal Lineal para detectar violaciones de seguridad y generar contraejemplos explicativos.

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

Publicado 2026-01-15

📖 5 min de lectura🧠 Análisis profundo

CC BY 4.0

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

Artículo original bajo licencia CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita ni avalada por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo

Imagina que tienes un asistente digital muy inteligente y paciente que vive con un adulto mayor. Este asistente no solo observa; intenta comprender el ritmo diario único, las preferencias y la disposición del hogar de la persona. El documento que compartiste describe un nuevo "libro de reglas" para construir este asistente, utilizando una mezcla de sensores del mundo real y lógica formal para garantizar que la persona viva de forma segura y feliz mientras mantiene su independencia.

Así es como funciona el marco de trabajo, desglosado en conceptos simples:

1. La configuración: Construir un Gemelo Digital

Piensa en el hogar de un adulto mayor como un rompecabezas complejo. Para entender cómo encajan las piezas del rompecabezas, los investigadores no se limitaron a pegar sensores en las paredes; primero se sentaron a charlar (una entrevista semiestructurada).

La Entrevista: Preguntaron a la persona sobre sus rutinas, lo que le gusta, lo que no le gusta (como las preocupaciones de privacidad en el dormitorio) y cómo se desplaza.
Los Sensores: Instalaron "ojos digitales" discretos (sensores de movimiento) y "sensores de tacto digital" (sensores de contacto en puertas, cajones y refrigeradores). Estos sensores actúan como el sistema nervioso de la casa, enviando pequeñas señales cada vez que se abre una puerta o alguien pasa por un lugar.
El Resultado: Combinaron las notas de la charla con los datos de los sensores para construir un Gemelo Digital Personalizado. Este no es un modelo genérico; es un mapa hecho a medida de la vida y el hogar de esa persona específica.

2. El Libro de Reglas: Escribir historias de "Si-Entonces"

Una vez que tuvieron el gemelo digital, necesitaban una forma de verificar si la persona estaba haciendo lo que habitualmente hace. En lugar de solo mirar los datos brutos, escribieron un "Libro de Reglas" utilizando un lenguaje especial llamado Lógica Temporal Lineal (LTL).

Piensa en esto como escribir una historia con puntos de la trama estrictos.

Ejemplo de Regla 1 (La ducha matutina): "Una vez que la persona se despierta y sale del dormitorio, debe eventualmente ir al pasillo, luego al baño y finalmente cerrar la puerta de la ducha".
Ejemplo de Regla 2 (La comida de la mascota): "Si se abre el refrigerador por la mañana, debe ocurrir antes de que se abran los armarios de la cocina". (Esto fue una preferencia específica para un participante que alimenta a sus mascotas antes del desayuno).
Ejemplo de Regla 3 (La medicina): "Para llegar a la medicina, la persona debe pasar primero por la sala de estar".

Estas reglas se escriben en un lenguaje matemático preciso que una computadora puede leer sin confundirse.

3. El Juez: El Verificador de Modelos

Aquí es donde ocurre la magia. Los investigadores utilizaron una herramienta llamada NuSMV, que actúa como un juez incansable y superrápido.

El juez toma el Gemelo Digital (el mapa de la casa y los sensores) y el Libro de Reglas (las reglas LTL).
Ejecuta el día de datos como una cinta de película, verificando cada escena contra las reglas.
Si se sigue la regla: El juez dice: "¡Todo despejado!".
Si se rompe la regla: No solo imprime un "Error". Imprime un Contraejemplo. Esto es como una "reproducción" que muestra exactamente dónde la historia se salió del guion.

4. Lo que encontraron (Los Resultados)

El equipo probó esto en dos personas diferentes (llamémoslas Participante A y Participante B) para ver si el sistema funcionaba.

El error del "Casi": Para el Participante A, la regla decía: "Dormitorio -> Pasillo -> Baño -> Puerta de la ducha cerrada". Una mañana, la persona fue Dormitorio -> Pasillo -> Baño -> Pasillo -> Baño -> Puerta de la ducha cerrada.
- La computadora marcó esto como una "violación" porque la persona regresó al pasillo.
- La Perspectiva: La persona sí se tomó una ducha, pero su rutina tuvo un pequeño desvío. El sistema detectó esto, mostrando que las reglas podrían necesitar ser ligeramente más flexibles para permitir pequeños y de ningún modo perjudiciales "zigzagueos" en la rutina.
El paso "Omitido": Para el Participante B, la regla era sobre tomar la medicina. La regla decía que debía pasar por la sala de estar para obtener la medicina. Un día, la persona no pasó por la sala de estar hasta después del intervalo de tiempo esperado.
- La Perspectiva: El sistema marcó esto como una violación. Esto es importante porque, a diferencia de una ducha, omitir un horario de medicación programado podría ser un riesgo de seguridad. El sistema identificó con éxito que la actividad ocurrió, pero no cuando se suponía que debía ocurrir.

5. La Conclusión

El artículo afirma que este marco de trabajo es una nueva y poderosa forma de monitorear a los adultos mayores. No se trata solo de vigilarlos; se trata de comprender su contexto específico.

Es Personal: Respeta la privacidad (al no usar cámaras) y se adapta a la casa y los hábitos específicos de la persona.
Es Preciso: Utiliza las matemáticas para demostrar si un comportamiento es "seguro" o "normal" para esa persona específica.
Es una Red de Seguridad: Puede detectar cuando alguien se desvía de su rutina, ya sea un cambio inofensivo (como tomar una ducha unos minutos más tarde) o una posible señal de alerta (como olvidar tomar una medicina).

Los investigadores concluyen que, si bien el sistema funciona bien, el comportamiento humano es caótico. A veces, un sensor ve un refrigerador abrirse, pero no sabemos si se consumió algún alimento. Sin embargo, al combinar los sensores con las propias historias y preferencias de la persona, este marco de trabajo ofrece una imagen mucho más clara y personalizada de su vida diaria que nunca antes.

Resumen Técnico: Un Marco de Verificación Formal Personalizado para el Monitoreo de Actividades de la Vida Diaria

Planteamiento del Problema
El artículo aborda la necesidad urgente de apoyar la calidad de vida (QoL) y la seguridad de una población creciente de adultos mayores (OAs) que viven de forma independiente. Si bien el monitoreo basado en sensores de las Actividades de la Vida Diaria (ADLs) está consolidado para detectar declives en la salud, los enfoques existentes suelen carecer de personalización. Muchos sistemas se basan en supuestos genéricos sobre rutinas y ubicaciones, fallando al no tener en cuenta las preferencias individuales, la disposición específica del hogar y las preocupaciones de privacidad. Además, los trabajos previos que utilizan métodos formales para el monitoreo de las ADLs se han limitado en gran medida a entornos controlados y simulados, en lugar de entornos domésticos del mundo real. El desafío central es desarrollar un sistema que pueda verificar rigurosamente si el comportamiento observado de un individuo se adhiere a sus requisitos específicos de seguridad y rutina sin imponer un modelo de "talla única".

Metodología
Los autores proponen un marco que integra datos de sensores comerciales no intrusivos con información contextual rica derivada de entrevistas semiestructuradas y observaciones sociológicas. La metodología avanza a través de las siguientes etapas:

Recolección de Datos:
- Cualitativa: Los investigadores realizan entrevistas semiestructuradas para mapear rutinas diarias, preferencias, límites de privacidad y necesidades específicas. Esto informa la colocación de los sensores y la definición de propiedades.
- Cuantitativa: Se despliegan sensores de contacto (monitoreo de puertas, cajones, electrodomésticos) y sensores de movimiento infrarrojo pasivo (PIR) en las casas de los participantes. Los datos se agregan a través de Home Assistant y se almacenan en InfluxDB.
- Participantes: El estudio involucró a 10 OAs (de 67 a 97 años) en Edimburgo, Escocia. El artículo presenta estudios de caso detallados de dos participantes (A y B) con rutinas contrastantes.
Preprocesamiento de Datos:
- Los datos de los sensores se limpian para eliminar el ruido (por ejemplo, fluctuaciones de temperatura en los sensores de contacto) y actualizaciones de estado redundantes.
- Los eventos de los sensores de movimiento se tratan como transiciones instantáneas, y se eliminan los estados de "limpio" (clear) a menos que marquen el final de una secuencia de movimiento.
- Los datos se segmentan en "subtrazas" de 20 minutos con solapamientos de 10 minutos para gestionar el problema de la explosión del espacio de estados inherente a la verificación de modelos.
Modelado Formal:
- Generación de Modelos: Una herramienta automatizada genera un sistema de transición de estados finitos (usando NuSMV) basado en la disposición del hogar del participante (representada como un grafo dirigido de habitaciones) y la configuración específica de los sensores.
- Representación de Estados: El modelo rastrea los estados de los sensores (abierto/cerrado, detectado/limpio) y el movimiento del participante entre habitaciones.
- Especificación de Propiedades: Los requisitos se codifican en Lógica Temporal Lineal pasada (pLTL), una extensión de la Lógica Temporal Lineal (LTL) que incluye operadores de tiempo pasado. Esto permite razonar sobre secuencias de eventos en relación con el tiempo actual. Las propiedades se derivan del análisis de las entrevistas y se categorizan como generales (por ejemplo, higiene), específicas del individuo (por ejemplo, cuidado de mascotas) o basadas en la rutina (por ejemplo, medicación).
Verificación:
- El verificador de modelos NuSMV verifica si el modelo generado satisface las propiedades pLTL.
- Si una propiedad se viola, NuSMV genera un contraejemplo (una secuencia específica de estados) para identificar la causa de la desviación.

Contribuciones Clave
El artículo describe tres contribuciones primarias:

Un Marco Integral: Integra la verificación de modelos formales con datos de sensores comerciales e información contextual explícita (entrevistas, disposiciones de hogares, observaciones) para crear modelos personalizados. Esto vincula los eventos de los sensores directamente con las preferencias y necesidades individuales.
Enfoque de Especificación Sistemática: Proporciona un método riguroso para derivar propiedades formales a partir de entrevistas semiestructuradas, asegurando que los criterios de verificación reflejen el contexto único de cada participante.
Generalizabilidad en Entornos del Mundo Real: El marco se demuestra en dos participantes distintos con diferentes ADLs, probando su adaptabilidad a diversas situaciones de vida y rutinas fuera de entornos de laboratorio controlados.

Resultos y Análisis
El marco se aplicó para verificar rutinas matutinas específicas para dos participantes:

Participante A: Las propiedades verificadas incluyeron una secuencia específica para ducharse (Dormitorio $\to$ $\to$ Pasillo $\to$ $\to$ Baño $\to$ $\to$ Puerta de la ducha cerrada) y una secuencia específica para alimentar a las mascotas (Refrigerador abierto antes que otros armarios).
- Hallazgos: La propiedad de la ducha se cumplió en la mayoría de los días, pero se violó una vez debido a una desviación menor (regresar al pasillo antes de cerrar la puerta de la ducha). La propiedad de alimentación de mascotas se violó una vez en un domingo, probablemente debido a un cambio en las rutinas de fin de semana.
Participante B: Una propiedad verificó la secuencia de moverse del salón a la cocina para acceder a un dispensador de medicamentos.
- Hallazgos: La propiedad se cumplió en la mayoría de los días, pero se violó un viernes cuando el participante accedió a la medicación después de la ventana de tiempo definida (9:50 AM frente a la ventana de 7:00–9:00 AM).

El análisis destaca que, si bien el marco identifica con éxito las desviaciones, algunas "violaciones" provienen de cambios de rutina menores y no críticos (por ejemplo, tomar una ducha un poco más tarde o en un orden diferente) en lugar de riesgos de seguridad. Por el contrario, las desviaciones en la toma programada de medicamentos se señalaron como posibles riesgos de seguridad. El estudio también señaló limitaciones, incluyendo fallos de los sensores (aproximadamente el 1% de los datos), ruido de mascotas/visitantes y la ambigüedad inherente de los eventos de los sensores (por ejemplo, abrir una nevera no garantiza el consumo de alimentos).

Significancia y Reivindicaciones
El artículo sostiene que este marco ofrece un enfoque novedoso y centrado en la persona para el monitoreo de las ADL que va más allá de las alertas de salud genéricas. Al combinar la verificación formal con el contexto cualitativo, el sistema puede:

Detectar comportamientos no anticipados a lo largo del tiempo.
Distinguir entre desviaciones de la rutina y posibles riesgos de seguridad.
Proporcionar un mecanismo para la intervención oportuna cuando se violan propiedades críticas (como la adherencia a la medicación).

Los autores mantienen una postura modesta, reconociendo que, aunque el marco muestra promesa para mejorar la seguridad y el bienestar, persisten desafíos con respecto a la interpretación de los datos de los sensores y la variabilidad del comportamiento humano. Concluyen que el enfoque es factible para el despliegue en el mundo real, pero requiere un refinamiento cuidadoso de los requisitos temporales para acomodar la flexibilidad natural de la vida cotidiana.