💻 computer science

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

Este artigo apresenta um framework de verificação formal personalizado que integra dados de sensores com o contexto individual para modelar e verificar formalmente Atividades da Vida Diária para idosos que vivem de forma independente, utilizando Lógica Temporal Linear para detectar violações de segurança e gerar contraexemplos explicativos.

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

Publicado 2026-01-15

📖 5 min de leitura🧠 Leitura aprofundada

CC BY 4.0

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

Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

Imagine que você tem um assistente digital muito inteligente e paciente vivendo com um idoso. Este assistente não apenas observa; ele tenta entender o ritmo diário único da pessoa, suas preferências e a disposição de sua casa. O artigo que você compartilhou descreve um novo "livro de regras" para construir este assistente, usando uma mistura de sensores do mundo real e lógica formal para garantir que a pessoa viva de forma segura e feliz enquanto mora de forma independente.

Aqui está como o framework funciona, dividido em conceitos simples:

1. A Configuração: Construindo um Gêmeo Digital

Pense na casa do idoso como um quebra-cabeça complexo. Para entender como as peças do quebra-cabeça se encaixam, os pesquisadores não apenas instalaram sensores nas paredes; eles primeiro sentaram para uma conversa (uma entrevista semiestruturada).

A Entrevista: Eles perguntaram à pessoa sobre suas rotinas, o que ela gosta, o que ela não gosta (como preocupações com privacidade no quarto) e como ela se movimenta.
Os Sensores: Eles instalaram "olhos digitais" discretos (sensores de movimento) e "sensores de toque digitais" (sensores de contato em portas, gavetas e geladeiras). Esses sensores atuam como o sistema nervoso da casa, enviando sinais minúsculos sempre que uma porta é aberta ou alguém passa por perto.
O Resultado: Eles combinaram as notas da conversa com os dados dos sensores para construir um Gêmeo Digital Personalizado. Este não é um modelo genérico; é um mapa feito sob medida para a vida e a casa de aquela pessoa específica.

2. O Livro de Regras: Escrevendo Histórias de "Se-Então"

Uma vez que tivessem o gêmeo digital, eles precisavam de uma maneira de verificar se a pessoa estava fazendo o que costuma fazer. Em vez de apenas olhar para dados brutos, eles escreveram um "Livro de Regras" usando uma linguagem especial chamada Lógica Temporal Linear (LTL).

Pense nisso como escrever uma história com pontos de enredo rigorosos.

Exemplo de Regra 1 (O Banho Matinal): "Uma vez que a pessoa acorde e saia do quarto, ela deve eventualmente ir para o corredor, depois para o banheiro e, finalmente, fechar a porta do chuveiro."
Exemplo de Regra 2 (A Comida do Pet): "Se a geladeira for aberta pela manhã, isso deve acontecer antes que quaisquer armários da cozinha sejam abertos." (Esta foi uma preferência específica de um participante que alimenta seus animais de estimação antes do café da manhã).
Exemplo de Regra 3 (O Remédio): "Para chegar ao remédio, a pessoa deve passar pela sala de estar primeiro."

Essas regras são escritas em uma linguagem matemática precisa que um computador pode ler sem se confundir.

3. O Juiz: O Verificador de Modelos

É aqui que a mágica acontece. Os pesquisadores usaram uma ferramenta chamada NuSMV, que atua como um juiz incansável e superveloz.

O juiz pega o Gêmeo Digital (o mapa da casa e dos sensores) e o Livro de Regras (as regras LTL).
Ele percorre os dados do dia como um rolo de filme, verificando cada cena contra as regras.
Se a regra for seguida: O juiz diz: "Tudo certo!"
Se a regra for quebrada: Ele não apenas diz "Erro". Ele imprime um Contraexemplo. Isso é como uma "reprodução" mostrando exatamente onde a história saiu do roteiro.

4. O Que Eles Descobriram (Os Resultados)

A equipe testou isso em duas pessoas diferentes (vamos chamá-las de Participante A e Participante B) para ver se o sistema funcionava.

O Erro "Quase": Para o Participante A, a regra era: "Quarto -> Corredor -> Banheiro -> Porta do Chuveiro Fechada". Em uma manhã, a pessoa foi Quarto -> Corredor -> Banheiro -> Corredor -> Banheiro -> Porta do Chuveiro Fechada.
- O computador sinalizou isso como uma "violação" porque a pessoa voltou para o corredor.
- O Insight: A pessoa realmente tomou banho, mas sua rotina teve um pequeno desvio. O sistema detectou isso, mostrando que as regras podem precisar ser um pouco mais flexíveis para permitir pequenos e inofensivos movimentos fora do padrão.
A Etapa "Perdida": Para o Participante B, a regra era sobre tomar o remédio. A regra dizia que eles devem passar pela sala de estar para pegar o remédio. Em um determinado dia, a pessoa não passou pela sala até depois do horário esperado.
- O Insight: O sistema sinalizou isso como uma violação. Isso é importante porque, ao contrário de um banho, esquecer o horário de um medicamento pode ser um risco à segurança. O sistema identificou com sucesso que a atividade aconteceu, mas não quando deveria ter ocorrido.

5. A Conclusão

O artigo afirma que este framework é uma nova e poderosa maneira de monitorar idosos. Não se trata apenas de observá-los; é sobre entender seu contexto específico.

É Pessoal: Respeita a privacidade (ao não usar câmeras) e se adapta à casa e aos hábitos específicos da pessoa.
É Preciso: Usa a matemática para provar se um comportamento é "seguro" ou "normal" para aquela pessoa específica.
É uma Rede de Segurança: Pode detectar quando alguém se desvia de sua rotina, seja uma mudança inofensiva (como tomar banho alguns minutos mais tarde) ou um possível sinal de alerta (como esquecer de tomar um remédio).

Os pesquisadores concluem que, embora o sistema funcione bem, o comportamento humano é caótico. Às vezes, um sensor vê uma geladeira abrir, mas não sabemos se comida foi consumida. No entanto, ao combinar os sensores com as próprias histórias e preferências da pessoa, este framework oferece uma imagem muito mais clara e personalizada de sua vida diária do que nunca antes.

Resumo Técnico: Uma Estrutura de Verificação Formal Personalizada para Monitoramento de Atividades da Vida Diária

Definição do Problema
O artigo aborda a necessidade urgente de apoiar a qualidade de vida (QoL) e a segurança de uma população crescente de idosos (OAs) que vivem de forma independente. Embora o monitoramento baseado em sensores das Atividades da Vida Diária (ADLs) seja estabelecido para detectar declínios de saúde, as abordagens existentes muitas vezes carecem de personalização. Muitos sistemas baseiam-se em pressupostos genéricos sobre rotinas e localizações, falhando em considerar preferências individuais, layouts específicos de residências e preocupações com a privacidade. Além disso, trabalhos anteriores utilizando métodos formais para o monitoramento de ADLs têm sido limitados majoritariamente a ambientes controlados e simulados, em vez de ambientes domésticos do mundo real. O desafio central é desenvolver um sistema que possa verificar rigorosamente se o comportamento observado de um indivíduo adere aos seus requisitos específicos de segurança e rotina sem impor um modelo de "tamanho único".

Metodologia
Os autores propõem uma estrutura que integra dados de sensores comerciais não intrusivos com informações contextuais ricas derivadas de entrevistas semiestruturadas e observações sociológicas. A metodologia procede através das seguintes etapas:

Coleta de Dados:
- Qualitativa: Os pesquisadores conduzem entrevistas semiestruturadas para mapear rotinas diárias, preferências, limites de privacidade e necessidades específicas. Isso informa o posicionamento dos sensores e a definição de propriedades.
- Quantitativa: Sensores de contato (monitorando portas, gavetas, eletrodomésticos) e sensores de movimento infravermelho passivo (PIR) são implantados nas casas dos participantes. Os dados são agregados via Home Assistant e armazenados no InfluxDB.
- Participantes: O estudo envolveu 10 idosos (67–97 anos) em Edimburgo, Escócia. O artigo apresenta estudos de caso detalhados de dois participantes (A e B) com rotinas contrastantes.
Pré-processamento de Dados:
- Os dados dos sensores são limpos para remover ruídos (ex: flutuações de temperatura em sensores de contato) e atualizações de estado redundantes.
- Eventos de sensores de movimento são tratados como transições instantâneas, com estados "clear" (limpo/ausente) removidos, a menos que marquem o fim de uma sequência de movimento.
- Os dados são segmentados em "subtraces" de 20 minutos com sobreposições de 10 minutos para gerenciar o problema de explosão do espaço de estados inerente à verificação de modelos (model checking).
Modelagem Formal:
- Geração de Modelo: Uma ferramenta automatizada gera um sistema de transição de estados finito (usando NuSMV) baseado no layout da casa do participante (representado como um grafo direcionado de cômodos) e na configuração específica dos sensores.
- Representação de Estado: O modelo rastreia os estados dos sensores (aberto/fechado, detectado/ausente) e o movimento do participante entre os cômodos.
- Especificação de Propriedades: Os requisitos são codificados em Lógica Temporal Linear do Passado (pLTL), uma extensão da Lógica Temporal Linear (LTL) que inclui operadores de tempo passado. Isso permite o raciocínio sobre sequências de eventos em relação ao tempo atual. As propriedades são derivadas da análise das entrevistas e categorizadas como gerais (ex: higiene), específicas do indivíduo (ex: cuidado com animais de estimação) ou baseadas em rotina (ex: medicação).
Verificação:
- O verificador de modelos NuSMV verifica se o modelo gerado satisfaz as propriedades pLTL.
- Se uma propriedade for violada, o NuSMV gera um contraexemplo (uma sequência específica de estados) para identificar a causa do desvio.

Principais Contribuições
O artigo delineia três contribuições primárias:

Uma Estrutura Abrangente: Integra a verificação de modelos formais com dados de sensores comerciais e informações contextuais explícitas (entrevistas, layouts de casas, observações) para criar modelos personalizados. Isso vincula eventos de sensores diretamente às preferências e necessidades individuais.
Abordagem de Especificação Sistemática: Fornece um método rigoroso para derivar propriedades formais a partir de entrevistas semiestruturadas, garantindo que os critérios de verificação reflitam o contexto único de cada participante.
Generalizabilidade em Cenários do Mundo Real: A estrutura é demonstrada em dois participantes distintos com diferentes ADLs, provando sua adaptabilidade a diversas situações de vida e rotinas fora de ambientes laboratoriais controlados.

Resultos e Análise
A estrutura foi aplicada para verificar rotinas matinais específicas para dois participantes:

Participante A: As propriedades verificadas incluíram uma sequência específica para o banho (Quarto $\to$ $\to$ Corredor $\to$ $\to$ Banheiro $\to$ $\to$ Porta do Banho Fechada) e uma sequência específica para alimentar os animais de estimação (Geladeira aberta antes de outros armários).
- Achados: A propriedade do banho foi satisfeita na maioria dos dias, mas violada uma vez devido a um desvio menor (retornar ao corredor antes de fechar a porta do banho). A propriedade de alimentação dos animais foi violada uma vez no domingo, provavelmente devido a uma mudança nas rotinas de fim de semana.
Participante B: Uma propriedade verificou a sequência de mover-se do lounge para a cozinha para acessar um dispensador de medicamentos.
- Achados: A propriedade foi satisfeita na maioria dos dias, mas violada em uma sexta-feira quando o participante acessou a medicação após a janela de tempo definida (9:50 AM vs. a janela de 7:00–9:00 AM).

A análise destaca que, embora a estrutura identifique com sucesso desvios, algumas "violações" decorrem de mudanças de rotina menores e não críticas (ex: tomar banho um pouco mais tarde ou em uma ordem diferente) em vez de riscos de segurança. Por outro vez, desvios na ingestão programada de medicamentos foram sinalizados como potenciais riscos de segurança. O estudo também observou limitações, incluindo falhas de sensores (aprox. 1% dos dados), ruído de animais de estimação/visitantes e a ambiguidade inerente aos eventos de sensores (ex: abrir uma geladeira não garante o consumo de alimentos).

Significância e Alegações
O artigo afirma que esta estrutura oferece uma abordagem inovadora e centrada na pessoa para o monitoramento de ADL que vai além de alertas de saúde genéricos. Ao combinar a verificação formal com o contexto qualitativo, o sistema pode:

Detectar comportamentos imprevistos ao longo do tempo.
Distinguir entre desvios de rotina e potenciais riscos de segurança.
Fornecer um mecanismo para intervenção oportuna quando propriedades críticas (como a adesão à medicação) são violadas.

Os autores mantêm uma postura modesta, reconhecendo que, embora a estrutura mostre promessa para aumentar a segurança e o bem-estar, permanecem desafios em relação à interpretação dos dados dos sensores e à variabilidade do comportamento humano. Eles concluem que a abordagem é viável para implantação no mundo real, mas requer o refinamento cuidadoso dos requisitos temporais para acomodar a flexibilidade natural da vida cotidiana.